lean_workbook_plus_9398
ProvedProve that if and , then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9398 (x y z : ℝ) (h : x + y + z >= x * y * z) : x ^ 2 + y ^ 2 + z ^ 2 >= x * y * z := by sorry
Source
Prove that if and , then
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_9398 (x y z : ℝ) (h : x + y + z >= x * y * z) : x ^ 2 + y ^ 2 + z ^ 2 >= x * y * z := by sorry