English
Dirichlet-type result: for coprime a and q, there are primes p with p ≡ a (mod q) and arbitrarily large.
Русский
Для пары взаимно простых a и q существуют простые p, удовлетворяющие p ≡ a (mod q), и таких p может быть бесконечно много.
LaTeX
$$$\\forall n, \\exists p>n \\, (p\\ prime) \\wedge p\\equiv a\\ [Z/qZ]$$$
Lean4
/-- **Dirichlet's Theorem** on primes in arithmetic progression: if `q` is a positive
integer and `a : ℤ` is coürime to `q`, then there are infinitely many prime numbers `p`
such that `p ≡ a mod q`. -/
theorem forall_exists_prime_gt_and_modEq (n : ℕ) {a : ℤ} (h : IsCoprime a q) : ∃ p > n, p.Prime ∧ p ≡ a [ZMOD q] :=
by
have : IsUnit (a : ZMod q) := by rwa [ZMod.coe_int_isUnit_iff_isCoprime, isCoprime_comm]
obtain ⟨p, hpn, hpp, heq⟩ := forall_exists_prime_gt_and_eq_mod this n
refine ⟨p, hpn, hpp, ?_⟩
simpa [← ZMod.intCast_eq_intCast_iff] using heq
