lean_workbook_plus_33256
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33256 (x y z : ℝ) : 4 * (x ^ 2 + y ^ 2 + z ^ 2) ≥ 4 * (x * y + y * z + x * z) := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_33256 (x y z : ℝ) : 4 * (x ^ 2 + y ^ 2 + z ^ 2) ≥ 4 * (x * y + y * z + x * z) := by sorry