English
If a^{p−1} ≡ 1 (mod p) and for every prime q dividing p−1 we have a^{(p−1)/q} ≠ 1 (mod p), then p is prime.
Русский
Если a^{p−1} ≡ 1 (mod p) и для каждого простого q, делящего p−1, выполняется a^{(p−1)/q} ≠ 1 (mod p), тогда p — простое.
LaTeX
$$$a^{p-1} \equiv 1 \pmod p \land \forall q \ (q\text{ prime} \rightarrow q \mid p-1 \rightarrow a^{(p-1)/q} \not\equiv 1 \pmod p) \Rightarrow p \text{ is prime}$$$
Lean4
/-- If `a^(p-1) = 1 mod p`, but `a^((p-1)/q) ≠ 1 mod p` for all prime factors `q` of `p-1`, then `p`
is prime. This is true because `a` has order `p-1` in the multiplicative group mod `p`, so this
group must itself have order `p-1`, which only happens when `p` is prime.
-/
theorem lucas_primality (p : ℕ) (a : ZMod p) (ha : a ^ (p - 1) = 1)
(hd : ∀ q : ℕ, q.Prime → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1) : p.Prime :=
by
have h : p ≠ 0 ∧ p ≠ 1 := by constructor <;> rintro rfl <;> exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
have hp1 : 1 < p := Nat.one_lt_iff_ne_zero_and_ne_one.2 h
have : NeZero p := ⟨h.1⟩
rw [Nat.prime_iff_card_units]
apply (Nat.card_units_zmod_lt_sub_one hp1).antisymm
let a' : (ZMod p)ˣ := Units.mkOfMulEqOne a _ (by rwa [← pow_succ', tsub_add_eq_add_tsub hp1])
calc
p - 1 = orderOf a := (orderOf_eq_of_pow_and_pow_div_prime (tsub_pos_of_lt hp1) ha hd).symm
_ = orderOf a' := (orderOf_injective (Units.coeHom _) Units.val_injective a')
_ ≤ Fintype.card (ZMod p)ˣ := orderOf_le_card_univ
