English
If p is prime and n is an integer coprime to p, then n^{p-1} ≡ 1 (mod p).
Русский
Если p — простое, и n целое число, coprime к p, то n^{p-1} ≡ 1 (mod p).
LaTeX
$$$\\\\forall p \\\\in \\\\mathbb{N}, \\\\text{Prime}(p) \\\\Rightarrow \\\\forall n \\\\in \\mathbb{Z}, \\\\gcd(n,p)=1 \\\\Rightarrow n^{p-1} \\\\equiv 1 \\\\pmod p$$$
Lean4
/-- **Fermat's Little Theorem**: for all `a : ℤ` coprime to `p`, we have
`a ^ (p - 1) ≡ 1 [ZMOD p]`. -/
theorem pow_card_sub_one_eq_one {p : ℕ} (hp : Nat.Prime p) {n : ℤ} (hpn : IsCoprime n p) : n ^ (p - 1) ≡ 1 [ZMOD p] :=
by
haveI : Fact p.Prime := ⟨hp⟩
have : ¬(n : ZMod p) = 0 :=
by
rw [CharP.intCast_eq_zero_iff _ p, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd]
· exact hpn.symm
simpa [← ZMod.intCast_eq_intCast_iff] using ZMod.pow_card_sub_one_eq_one this
