Theorems · Theorem · number theory

IsCyclic.monoidHom_equiv_self

∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [Finite G] [IsCyclic G] [inst_3 : CommMonoid M]
  [HasEnoughRootsOfUnity M (Nat.card G)], Nonempty ((G →* Mˣ) ≃* G)

The group of group homomorphisms from a finite cyclic group G of order n into the group of units of a ring M with all roots of unity is isomorphic to G

Defined in

Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Cited by

1 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupFiniteIsCyclicCommMonoidHasEnoughRootsOfUnity