feat(cyclotomic/basic): diverse roots of unity lemmas (#11473)
feat(cyclotomic/basic): diverse roots of unity lemmas (#11473)

From flt-regular.





leanprover-community/mathlib,leanprover-community/mathlib