lean_workbook_plus_36423

Proved

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

Prove that $n^{2225} - n^{2005} = n^{2005}(n^{220}-1)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36423 (n : ℕ) : n^2225 - n^2005 = n^2005 * (n^220 - 1)   :=  by sorry

Source