Theorems · Inductive type · number theory

HasEnoughRootsOfUnity

(M : Type u_1) → [CommMonoid M] → ℕ → Prop

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

Cited by

56 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CommMonoid