Theorems · Theorem · number theory

IsCyclic.monoidHom_mulEquiv_rootsOfUnity

∀ (G : Type u_7) [inst : CommGroup G] [IsCyclic G] (G' : Type u_8) [inst_2 : CommGroup G'],
  Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))

The group of group homomorphisms from a finite cyclic group G of order n into another group G' is (noncanonically) isomorphic to the group of nth roots of unity in G'.

Defined in

Mathlib.RingTheory.RootsOfUnity.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommGroupIsCyclicCommGroup