mulAutMulEquiv — Mathlib

English

The automorphism group of a cyclic group is isomorphic to the unit group of ZMod card.

Русский

Автоморфизмная группа циклической группы изоморфна группе единиц ZMod порядков группы.

LaTeX

$$$\mathrm{MulAut}(G) \cong^* (\mathbb{Z}/n\mathbb{Z})^{\times}$,\; n=|G|,\; G\text{ cyclic}$$

Lean4

/-- The automorphism group of a cyclic group is isomorphic to the multiplicative group of ZMod. -/
@[simps!]
noncomputable def mulAutMulEquiv [Group G] [h : IsCyclic G] : MulAut G ≃* (ZMod (Nat.card G))ˣ :=
  ((MulAut.congr (zmodCyclicMulEquiv h)).symm.trans (MulAutMultiplicative (ZMod (Nat.card G)))).trans
    (ZMod.AddAutEquivUnits (Nat.card G))

Похожие утверждения