Mathlib.Data.ZMod.Aut

: AddAut (ZMod n) ≃* (ZMod n)ˣ

Full source

/-- The automorphism group of `ZMod n` is isomorphic to the group of units of `ZMod n`. -/
@[simps]
def AddAutEquivUnits : AddAutAddAut (ZMod n) ≃* (ZMod n)ˣ :=
  have h (f : AddAut (ZMod n)) (x : ZMod n) : f 1 * x = f x := by
    rw [mul_comm, ← x.intCast_zmod_cast, ← zsmul_eq_mul, ← map_zsmul, zsmul_one]
  { toFun := fun f ↦ Units.mkOfMulEqOne (f 1) (f⁻¹ 1) ((h f _).trans (f.inv_apply_self _ _))
    invFun := AddAut.mulLeft
    left_inv := fun f ↦ by simp [DFunLike.ext_iff, Units.smul_def, h]
    right_inv := fun x ↦ by simp [Units.ext_iff, Units.smul_def]
    map_mul' := fun f g ↦ by simp [Units.ext_iff, h] }

Isomorphism between additive automorphisms and units of \( \mathbb{Z}/n\mathbb{Z} \)

Informal description

The automorphism group of the additive group of integers modulo \( n \) is isomorphic to the multiplicative group of units of \( \mathbb{Z}/n\mathbb{Z} \). Specifically, there is a multiplicative equivalence between the group of additive automorphisms of \( \mathbb{Z}/n\mathbb{Z} \) and the group of invertible elements of \( \mathbb{Z}/n\mathbb{Z} \).