mathlib

4a153ed9 - feat(ring_theory/polynomials/cyclotomic): add lemmas about cyclotomic polynomials (#5122)

feat(ring_theory/polynomials/cyclotomic): add lemmas about cyclotomic polynomials (#5122) Two lemmas about cyclotomic polynomials: `cyclotomic_of_prime` is the explicit formula for `cyclotomic p R` when `p` is prime; `cyclotomic_coeff_zero` shows that the constant term of `cyclotomic n R` is `1` if `2 ≤ n`. I will use this to prove that there are infinitely many prime congruent to `1` modulo `n`, for all `n`.