lean_workbook_plus_40868
Provedprove that:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_40868 (x y z : ℝ) : 5.3 + y^2 * x^2 + y^2 * z^2 + z^2 * x^2 ≥ 2 * (x * y + z * x + y * z) := by sorry
Source
prove that:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_40868 (x y z : ℝ) : 5.3 + y^2 * x^2 + y^2 * z^2 + z^2 * x^2 ≥ 2 * (x * y + z * x + y * z) := by sorry