lean_workbook_plus_65403

Proved

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

Prove that if $x$ and $y$ are positive integers where $x>1$ , then $x^y-1$ is divisible by $x-1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65403 (x y : ℕ) (hx : 1 < x) : (x - 1) ∣ (x^y - 1)   :=  by sorry

Source