Commit 2020-11-27 21:26 4a153ed9

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.