lean_workbook_plus_32376

Proved

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

Prove for all natural numbers $n$ and integer $x\neq1$ , $x^n-1$ is divisible by $x-1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32376 (x : ℤ) (n : ℕ) (hx: x ≠ 1) : x - 1 ∣ x ^ n - 1   :=  by sorry

Source