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

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

source
theorem nat.frequently_at_top_modeq_one {k : ℕ} (hk0 : k ≠ 0) :
∃ᶠ (p : ℕ) in filter.at_top, nat.prime p ∧ p ≡ 1 [MOD k]
source
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].