lean_workbook_plus_82162
Provedproofwiki
Prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_82162 {a b c : ℝ} : 0.5 * ((a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2) ≥ 0 := by sorrySource
Prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_82162 {a b c : ℝ} : 0.5 * ((a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2) ≥ 0 := by sorry