Theorems · Theorem · number theory

Nat.forall_exists_prime_gt_and_eq_mod

∀ {q : ℕ} [NeZero q] {a : ZMod q}, IsUnit a → ∀ (n : ℕ), ∃ p > n, Nat.Prime p ∧ ↑p = a

Dirichlet's Theorem on primes in arithmetic progression: if q is a positive integer and a : ZMod q is a unit, then there are infinitely many prime numbers p such that (p : ZMod q) = a.

Defined in

Mathlib.NumberTheory.LSeries.PrimesInAP

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZero