Commit 2024-11-06 07:46 ea4bde99

feat(RingTheory/RootsOfUnity/EnoughRootsOfUnity): new file (#18681) This PR adds a new file RingTheory.RootsOfUnity.EnoughRootsOfUnity that defines the type class HasEnoughRootsOfUnity, where HasEnoughRootsOfUnity M n for a commutative monoid M and a natural number n records that M has a primitive nth root of unity and the group of nth roots of unity in M is cyclic. Some relevant API is also provided. This property is the relevant one when considering the dual of an abelian group G via Hom(G, M) (here n is the exponent of G).