frequently_atTop_modEq_one — Mathlib

English

There are infinitely many primes p with p ≡ 1 (mod k).

Русский

Существует бесконечно много простых p, удовлетворяющих p ≡ 1 (mod k).

LaTeX

$$$\{p \in \mathbb{N} \mid \operatorname{Prime}(p) \wedge p \equiv 1 \pmod{k}\}$ бесконечно.$$

Lean4

theorem frequently_atTop_modEq_one {k : ℕ} (hk0 : k ≠ 0) : ∃ᶠ p in atTop, Nat.Prime p ∧ p ≡ 1 [MOD k] :=
  by
  refine frequently_atTop.2 fun n => ?_
  obtain ⟨p, hp⟩ := exists_prime_gt_modEq_one n hk0
  exact ⟨p, ⟨hp.2.1.le, hp.1, hp.2.2⟩⟩

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