infinite_setOf_prime_modEq_one — Mathlib

English

For any k ≠ 0, the set {p : Nat | Prime(p) ∧ p ≡ 1 [MOD k]} is infinite.

Русский

Для любого k ≠ 0 множество {p : Nat | Prime(p) ∧ p ≡ 1 [MOD k]} бесконечно.

LaTeX

$$Set.Infinite {p : \mathbb{N} | \operatorname{Prime}(p) ∧ p \equiv 1 \pmod{k}}$$

Lean4

/-- For any positive `k : ℕ` there are infinitely many primes `p` such that `p ≡ 1 [MOD k]`. -/
theorem infinite_setOf_prime_modEq_one {k : ℕ} (hk0 : k ≠ 0) : Set.Infinite {p : ℕ | Nat.Prime p ∧ p ≡ 1 [MOD k]} :=
  frequently_atTop_iff_infinite.1 (frequently_atTop_modEq_one hk0)

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