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].

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].

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