lean_workbook_plus_61375

Proved

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

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

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61375 (a b c : ℝ) (h : a + b + c = 0) : (a^2 + b^2 + c^2) / 2 * (a^5 + b^5 + c^5) / 5 = (a^7 + b^7 + c^7) / 7   :=  by sorry

Source

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

View graph