Commit 2020-11-06 14:57 91f8e687

feat(src/ring_theory/polynomial/cyclotomic): cyclotomic polynomials (#4914) I have added some basic results about cyclotomic polynomials. I defined them as the polynomial, with integer coefficients, that lifts the complex polynomial ∏ μ in primitive_roots n ℂ, (X - C μ). I proved that the degree of cyclotomic n is totient n and the product formula for X ^ n - 1. I plan to prove the irreducibility in the near future. This was in 4869 before I splitted that PR. Compared to it, I added the definition of cyclotomic n R for any ring R (still using the polynomial with coefficients in ℤ) and some easy lemmas, especially cyclotomic_of_ring_hom, cyclotomic'_eq_X_pow_sub_one_div cyclotomic_eq_X_pow_sub_one_div, and cycl_eq_cycl'.