lean_workbook_plus_3408

Proved

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

For any $a,b,c$ the following identity is true: $(a + b - c)\,(a - b + c) = \frac {1}{4}\left(\,6\,(ab + ac + bc) - 5\,(a^2 + b^2 + c^2) + (b + c - 3\,a)^2\right)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3408 (a b c : ℝ) : (a + b - c) * (a - b + c) = 1 / 4 * (6 * (a * b + a * c + b * c) - 5 * (a ^ 2 + b ^ 2 + c ^ 2) + (b + c - 3 * a) ^ 2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph