English
The automorphism group of a cyclic group is isomorphic to the units of ZMod(n).
Русский
automorphism группа циклической группы изоморфна единицамZMod(n).
LaTeX
$$\mathrm{MulAut}(G) \cong^* (\mathbb{Z}/n\mathbb{Z})^{\times}, \; n=|G|, \; G \text{ cyclic}$$
Lean4
/-- Given two groups that are generated by elements `g` and `g'` of the same order,
we obtain an isomorphism sending `g` to `g'`. -/
@[to_additive /-- Given two additive groups that are generated by elements `g` and `g'` of the same order,
we obtain an isomorphism sending `g` to `g'`. -/
]
noncomputable def mulEquivOfOrderOfEq : G ≃* G' := by
refine
MonoidHom.toMulEquiv (monoidHomOfForallMemZpowers hg h.symm.dvd) (monoidHomOfForallMemZpowers hg' h.dvd) ?_
?_ <;>
refine (MonoidHom.eq_iff_eq_on_generator (by assumption) _ _).mpr ?_ <;>
simp only [MonoidHom.coe_comp, Function.comp_apply, monoidHomOfForallMemZpowers_apply_gen, MonoidHom.id_apply]
