lean_workbook_plus_46871

Proved

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

prove that $\frac{a^7+b^7+c^7}{7}=\frac{a^5+b^5+c^5}{5}\cdot\frac{a^2+b^2+c^2}{2}$ if $a+b+c=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46871 : ∀ a b c : ℝ, a + b + c = 0 → (a^7 + b^7 + c^7) / 7 = (a^5 + b^5 + c^5) / 5 * (a^2 + b^2 + c^2) / 2   :=  by sorry

Source