lean_workbook_plus_71297

Proved

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

Prove $(a^3+b^3+c^3-3abc)(p^3+q^3+r^3-3pqr)=(u^3+v^3+w^3-3uvw)$ where $u=ap+br+cq$ , $v=aq+bp+cr$ , $w=ar+bq+cp$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71297 (a b c p q r u v w : ℤ) (hu : u = a * p + b * r + c * q) (hv : v = a * q + b * p + c * r) (hw : w = a * r + b * q + c * p) : (a ^ 3 + b ^ 3 + c ^ 3 - 3 * a * b * c) * (p ^ 3 + q ^ 3 + r ^ 3 - 3 * p * q * r) = u ^ 3 + v ^ 3 + w ^ 3 - 3 * u * v * w   :=  by sorry

Source

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

View graph