Structures · Algebra

HasEnoughRootsOfUnity

This is a type class recording that a commutative monoid M contains primitive nth roots of unity and such that the group of nth roots of unity is cyclic. Such monoids are suitable targets in the context of duality statements for groups of exponent n.

Defined in

Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Shape

2 explicit arguments · adds prim, cyc