English
Prime p iff there exists a in ZMod p with a^{p−1} = 1 and ∀ q prime, q | (p−1) implies a^{(p−1)/q} ≠ 1.
Русский
Число p простое тогда и только тогда, когда существует a в ZMod p такое, что a^{p−1} = 1 и для всех простых q, делящих p−1, a^{(p−1)/q} ≠ 1.
LaTeX
$$$p \text{ prime} \iff \exists a \in \mathbb{Z}/p\mathbb{Z}, a^{p-1} = 1 \land \forall q \ (q\text{ prime} \rightarrow q \mid p-1 \rightarrow a^{(p-1)/q} \neq 1)$$$
Lean4
/-- A number `p` is prime if and only if 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`.
-/
theorem lucas_primality_iff (p : ℕ) :
p.Prime ↔ ∃ a : ZMod p, a ^ (p - 1) = 1 ∧ ∀ q : ℕ, q.Prime → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1 :=
⟨reverse_lucas_primality p, fun ⟨a, ⟨ha, hb⟩⟩ ↦ lucas_primality p a ha hb⟩
