lean_workbook_plus_50578

Proved

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

If $x+y+z = 0$ , prove that $(x^2 + y^2 + z^2)/2 *(x^5 + y^5 + z^5)/5 = (x^7 + y^7 + z^7)/7$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50578 (x y z: ℝ) (hx: x + y + z = 0): (x^2 + y^2 + z^2) / 2 * (x^5 + y^5 + z^5) / 5 = (x^7 + y^7 + z^7) / 7   :=  by sorry

Source