lean_workbook_plus_27946

Proved

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

If $p$ is odd, then $a^p\equiv a\equiv 1\mod p$ implies $p$ divides $a-1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27946 (p a : ℕ) (hp : Odd p) : a^p ≡ a [ZMOD p] ∧ a ≡ 1 [ZMOD p] → p ∣ a - 1   :=  by sorry

Source