lean_workbook_plus_67097

Proved

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

Given $b^{2}-ab+{a^{2}\over 4}={b^{2}+c^{2}\over 2}-{a^{2}\over 4}$ , prove that $c^{2}=(b-a)^{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67097 : ∀ a b c : ℂ, b^2 - a * b + a^2 / 4 = (b^2 + c^2) / 2 - a^2 / 4 → c^2 = (b - a)^2   :=  by sorry

Source