English
For a finite cyclic group G, there exists a MulEquiv between monoid homomorphisms G →* G′ and the nth roots of unity in G′.
Русский
Для конечной циклической группы G существует муль-эквивалент между моноидными гомоморфизмами G →* G′ и n-й корней единицы в G′.
LaTeX
$$$\exists (\text{MulEquiv } (G \to^* G') (\operatorname{rootsOfUnity}(\lvert G \rvert) G'))$$$
Lean4
/-- 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 `n`th roots of unity in `G'`. -/
theorem monoidHom_mulEquiv_rootsOfUnity (G : Type*) [CommGroup G] [IsCyclic G] (G' : Type*) [CommGroup G'] :
Nonempty <| (G →* G') ≃* rootsOfUnity (Nat.card G) G' :=
by
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
exact ⟨monoidHomMulEquivRootsOfUnityOfGenerator hg G'⟩
