English
If p is prime, there exists a generator a of the multiplicative group modulo p such that a^{p−1} = 1 and a^{(p−1)/q} ≠ 1 for all prime q | (p−1).
Русский
Если p — простое число, существует порождающий элемент a в группе единиц mod p, такой что a^{p−1} = 1 и a^{(p−1)/q} ≠ 1 для всех простых q, делящих p−1.
LaTeX
$$$\exists a \in (\mathbb{Z}/p\mathbb{Z})^{\times}, a^{p-1} = 1 \land \forall q\ (q\text{ prime} \rightarrow q \mid p-1 \rightarrow a^{(p-1)/q} \neq 1)$$$
Lean4
/-- If `p` is prime, then there exists an `a` such that `a^(p-1) = 1 mod p`
and `a^((p-1)/q) ≠ 1 mod p` for all prime factors `q` of `p-1`.
The multiplicative group mod `p` is cyclic, so `a` can be any generator of the group
(which must have order `p-1`).
-/
theorem reverse_lucas_primality (p : ℕ) (hP : p.Prime) :
∃ a : ZMod p, a ^ (p - 1) = 1 ∧ ∀ q : ℕ, q.Prime → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1 :=
by
have : Fact p.Prime := ⟨hP⟩
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := (ZMod p)ˣ)
have h1 : orderOf g = p - 1 := by
rwa [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card, ← Nat.prime_iff_card_units]
have h2 := tsub_pos_iff_lt.2 hP.one_lt
rw [← orderOf_injective (Units.coeHom _) Units.val_injective _, orderOf_eq_iff h2] at h1
refine ⟨g, h1.1, fun q hq hqd ↦ ?_⟩
replace hq := hq.one_lt
exact h1.2 _ (Nat.div_lt_self h2 hq) (Nat.div_pos (Nat.le_of_dvd h2 hqd) (zero_lt_one.trans hq))
