lean_workbook_plus_7528
Provedprove
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7528 (x y z : ℝ) : x * y + z * x ≤ x ^ 2 + (y ^ 2 + z ^ 2) / 2 := by sorry
Source
prove
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_7528 (x y z : ℝ) : x * y + z * x ≤ x ^ 2 + (y ^ 2 + z ^ 2) / 2 := by sorry