lean_workbook_plus_39448

Proved

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

Let $x = a-b$ and $y = b-c$ . Then $(a-b)(b-c)(c-a) = -xy(x+y)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39448 (a b c x y : ℝ) (h₁ : x = a - b) (h₂ : y = b - c) : (a - b) * (b - c) * (c - a) = -x * y * (x + y)   :=  by sorry

Source