lean_workbook_plus_59138

Proved

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

Prove the identity\n\n $\frac{a^5+b^5+c^5}{5}=(\frac{a^2+b^2+c^2}{2})(\frac{a^3+b^3+c^3}{3})$ \n\nGiven: $a+b+c=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59138 {a b c : ℝ} (h : a + b + c = 0) :
  (a^5 + b^5 + c^5) / 5 = (a^2 + b^2 + c^2) / 2 * (a^3 + b^3 + c^3) / 3   :=  by sorry

Source

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

View graph