lean_workbook_plus_68439
Proved3(x^2+y^2+z^2) \ge (x+y+z)^2 so
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68439 : ∀ x y z : ℝ, (x + y + z) ^ 2 ≤ 3 * (x ^ 2 + y ^ 2 + z ^ 2) := by sorry
Source
3(x^2+y^2+z^2) \ge (x+y+z)^2 so
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_68439 : ∀ x y z : ℝ, (x + y + z) ^ 2 ≤ 3 * (x ^ 2 + y ^ 2 + z ^ 2) := by sorry