mathlib3

128b316c - feat(number_theory/primes_congruent_one): infinitely many primes congruent to 1 (#5217)

feat(number_theory/primes_congruent_one): infinitely many primes congruent to 1 (#5217) I prove that, for any positive `k : ℕ`, there are infinitely many primes `p` such that `p ≡ 1 [MOD k]`. I am not sure that `p ≡ 1 [MOD k]` is the recommended way of stating this in mathlib (instead of using `nat.cast_ring_hom `), I can change it if needed. Also, I don't know if it is appropriate to create a new file, but I didn't see any reasonable location.