lean_workbook_plus_24732

Proved

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

Show that if $x+y+z=0$ then $\frac{x^5+y^5+z^5}{5}=\frac{x^2+y^2+z^2}{2} \times \frac{x^3+y^3+z^3}{3}$ and $\frac{x^7+y^7+z^7}{7}=\frac{x^5+y^5+z^5}{5} \times \frac{x^2+y^2+z^2}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24732 (x y z : ℝ) (h : x + y + z = 0) : (x^5 + y^5 + z^5)/5 = (x^2 + y^2 + z^2)/2 * (x^3 + y^3 + z^3)/3 ∧ (x^7 + y^7 + z^7)/7 = (x^5 + y^5 + z^5)/5 * (x^2 + y^2 + z^2)/2   :=  by sorry

Source

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

View graph