mathlib documentation

number_theory.primes_congruent_one

Primes congruent to one #

We prove that, for any positive k : ℕ, there are infinitely many primes p such that p ≡ 1 [MOD k].

source
theorem nat.exists_prime_ge_modeq_one {k : ℕ} (n : ℕ) (hpos : 0 < k) :
∃ (p : ℕ), nat.prime p ∧ n ≤ p ∧ p ≡ 1 [MOD k]

For any positive k : ℕ there are infinitely many primes p such that p ≡ 1 [MOD k].

source
theorem nat.frequently_at_top_modeq_one {k : ℕ} (hpos : 0 < k) :
∃ᶠ (p : ℕ) in filter.at_top, nat.prime p ∧ p ≡ 1 [MOD k]
source
theorem nat.infinite_set_of_prime_modeq_one {k : ℕ} (hpos : 0 < k) :
{p : ℕ | nat.prime p ∧ p ≡ 1 [MOD k]}.infinite