lean_workbook_plus_82124
Provedproofwiki
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_82124 (x y z: ℝ) : (x^2 + y^2 + z^2 - x * y - x * z - y * z)^2 ≥ 0 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_82124 (x y z: ℝ) : (x^2 + y^2 + z^2 - x * y - x * z - y * z)^2 ≥ 0 := by sorry