Theorems · Theorem · number theory

reverse_lucas_primality

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

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).

Defined in

Mathlib.NumberTheory.LucasPrimality

Cited by

1 results in Mathlib

Foundations

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