Prove2Me

lean_workbook_plus_3175

Proved

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

(x2n+2−y2n+2)=(x2n−y2n)x2+y2n(x2−y2)(x^{2n + 2} - y^{2n + 2}) = (x^{2n} - y^{2n})x^2 + y^{2n}(x^2 - y^2)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3175 (x y : ℝ) (n : ℕ) : (x^(2 * n + 2) - y^(2 * n + 2)) = (x^(2 * n) - y^(2 * n)) * x^2 + y^(2 * n) * (x^2 - y^2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph