mathlib3 documentation

number_theory.primes_congruent_one

Primes congruent to one #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem nat.exists_prime_gt_modeq_one {k : } (n : ) (hk0 : k 0) :
(p : ), nat.prime p n < p p 1 [MOD k]

For any positive k : ℕ there exists an arbitrarily large prime p such that p ≡ 1 [MOD k].

theorem nat.infinite_set_of_prime_modeq_one {k : } (hk0 : k 0) :
{p : | nat.prime p p 1 [MOD k]}.infinite

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