lean_workbook_plus_80546

Proved

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

If $x+y+z=0$ then $2(x^5+y^5+z^5)=5xyz(x^2+y^2+z^2)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80546  (x y z : ℂ)
  (h₀ : x + y + z = 0) :
  2 * (x^5 + y^5 + z^5) = 5 * x * y * z * (x^2 + y^2 + z^2)   :=  by sorry

Source