lean_workbook_plus_35887

Proved

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

Show that $(a^3+b^3+c^3-3abc)(x^3+y^3+z^3-3xyz) = A^3+B^3+C^3-3ABC$ , where $A=ax+by+cz, B=ay+bz+cx, C=az+bx+cy$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35887 {a b c x y z A B C : ℂ} (ha : A = a * x + b * y + c * z) (hb : B = a * y + b * z + c * x) (hc : C = a * z + b * x + c * y) : (a ^ 3 + b ^ 3 + c ^ 3 - 3 * a * b * c) * (x ^ 3 + y ^ 3 + z ^ 3 - 3 * x * y * z) = A ^ 3 + B ^ 3 + C ^ 3 - 3 * A * B * C   :=  by sorry

Source

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

View graph