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 : ℕ), p.Prime ∧ n < p ∧ k.ModEq p 1

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, p.Prime ∧ k.ModEq p 1

theorem Nat.infinite_setOf_prime_modEq_one {k : ℕ} (hk0 : k ≠ 0) : {p : ℕ | p.Prime ∧ k.ModEq p 1}.Infinite

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