lean_workbook_plus_82230

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwiki

Add the 3 equality, we have ${a^2} + {b^2} + {c^2} = ab + bc + ca \Leftrightarrow \sum {{{\left( {a - b} \right)}^2}} = 0 \Leftrightarrow a = b = c$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82230 (a b c: ℝ): a^2 + b^2 + c^2 = a * b + b * c + c * a ↔ a = b ∧ b = c   :=  by sorry

Source