Documentation

Mathlib.NumberTheory.PrimesCongruentOne

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_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.frequently_atTop_modEq_one {k : } (hk0 : k 0) :
∃ᶠ (p : ) in Filter.atTop, Nat.Prime p p 1 [MOD k]
theorem Nat.infinite_setOf_prime_modEq_one {k : } (hk0 : k 0) :

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