Automorphism Group of ZMod.

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' := ⋯ }

@[simp]

theorem ZMod.AddAutEquivUnits_apply (n : ℕ) (f : AddAut (ZMod n)) : (AddAutEquivUnits n) f = Units.mkOfMulEqOne (f 1) (f⁻¹ 1) ⋯

@[simp]

theorem ZMod.AddAutEquivUnits_symm_apply (n : ℕ) (a : (ZMod n)ˣ) : (AddAutEquivUnits n).symm a = AddAut.mulLeft a