# Automorphism Group of `ZMod`. #

source
def ZMod.AddAutEquivUnits (n : ℕ) :
AddAut (ZMod n) ≃* (ZMod n)ˣ

The automorphism group of `ZMod n` is isomorphic to the group of units of `ZMod n`.

Equations

- ZMod.AddAutEquivUnits n = { toFun := fun (f : AddAut (ZMod n)) => Units.mkOfMulEqOne (f 1) (f⁻¹ 1) ⋯, invFun := ⇑AddAut.mulLeft, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem ZMod.AddAutEquivUnits_apply (n : ℕ) (f : AddAut (ZMod n)) :
(AddAutEquivUnits n) f = Units.mkOfMulEqOne (f 1) (f⁻¹ 1) ⋯
source
@[simp]
theorem ZMod.AddAutEquivUnits_symm_apply (n : ℕ) (a : (ZMod n)ˣ) :
(AddAutEquivUnits n).symm a = AddAut.mulLeft a