lucas_primality

theorem lucas_primality : ∀ (p : ℕ) (a : ZMod p), a ^ (p - 1) = 1 → (∀ (q : ℕ), q.Prime → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1) → p.Prime := by sorry

The Lucas Primality Theorem states that for any natural number `p` and an integer `a` modulo `p`, if `a` raised to the power of `p - 1` equals `1` modulo `p`, and for all prime numbers `q` that are divisors of `p - 1`, `a` raised to the power of `(p - 1) / q` does not equal `1` modulo `p`, then `p` is prime. This is because `a` has the order `p - 1` in the multiplicative group modulo `p`, therefore this group must have the order `p - 1` itself, which only happens when `p` is a prime number.

More concisely: If a natural number `p` is such that for all integers `a` with `gcd(a, p) = 1`, `a` raises to the power of `p-1` equals `1` modulo `p` only if `p` is a prime number, then `p` is prime.