Commit 2020-10-23 10:15 82b4843c

feat(ring_theory/roots_of_unity): Roots of unity as union of primitive roots (#4644) I have added some lemmas about roots of unity, especially root_of_unity_eq_uniun_prim that says that, if there is a primitive n-th root of unity in R, then the set of n-th roots of unity is equal to the union of primitive_roots i R for i | n. I will use this lemma in to develop the theory of cyclotomic polynomials.