Theorems · Definition · number theory

IsPrimitiveRoot.toRootsOfUnity

{M : Type u_1} → [inst : CommMonoid M] → {μ : M} → {n : ℕ} → [NeZero n] → IsPrimitiveRoot μ n → ↥(rootsOfUnity n M)

Turn a primitive root μ into a member of the rootsOfUnity subgroup.

Defined in

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Cited by

9 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext

Assumes

CommMonoidNeZero