mathlib

82b4843c - feat(ring_theory/roots_of_unity): Roots of unity as union of primitive roots (#4644)

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.