lean_workbook_plus_81029

Proved

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

we know that there is an $x$ s.t. $p^k|x^{p-1}-1$ (we can construct such solutions by induction on $k$ , for example)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81029 (p k : ℕ) : ∃ x : ℕ, p ^ k ∣ x ^ (p - 1) - 1   :=  by sorry

Source