lean_workbook_plus_7666
Provedholds for real .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7666 : ∀ (x y z : ℝ), 3 * (x ^ 2 + y ^ 2 + z ^ 2) ≥ (x + y + z) ^ 2 := by sorry
Source
holds for real .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_7666 : ∀ (x y z : ℝ), 3 * (x ^ 2 + y ^ 2 + z ^ 2) ≥ (x + y + z) ^ 2 := by sorry