Theorems · Theorem · number theory

lucas_primality

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

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.

Defined in

Mathlib.NumberTheory.LucasPrimality

Cited by

2 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound