lean_workbook_plus_37513
ProvedProve that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37513 : ∀ x y z : ℝ, 3 * (x * y + y * z + z * x) ≤ (x + y + z) ^ 2 := by sorry
Source
Prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_37513 : ∀ x y z : ℝ, 3 * (x * y + y * z + z * x) ≤ (x + y + z) ^ 2 := by sorry