forall_exists_prime_gt_and_eq_mod

English

There exist primes in an arithmetic progression: for any unit a mod q and any n, there is a prime p > n with p ≡ a (mod q).

Русский

Существуют простые числа в арифметической прогрессии: для любого единичного a по модулю q и любого n найдётся простое p > n такое, что p ≡ a (mod q).

LaTeX

$$$\\exists p>n\\; (p\\text{ prime} \\wedge p\\equiv a\\pmod q)$$$

Lean4

/-- **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`. -/
theorem forall_exists_prime_gt_and_eq_mod (ha : IsUnit a) (n : ℕ) : ∃ p > n, p.Prime ∧ (p : ZMod q) = a :=
  by
  obtain ⟨p, hp₁, hp₂⟩ := Set.infinite_iff_exists_gt.mp (setOf_prime_and_eq_mod_infinite ha) n
  exact ⟨p, hp₂.gt, Set.mem_setOf.mp hp₁⟩

Похожие утверждения