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
@[simp]
theorem
ZMod.AddAutEquivUnits_apply
(n : ℕ)
(f : AddAut (ZMod n))
:
(ZMod.AddAutEquivUnits n) f = Units.mkOfMulEqOne (f 1) (f⁻¹ 1) ⋯
@[simp]
theorem
ZMod.AddAutEquivUnits_symm_apply
(n : ℕ)
(a : (ZMod n)ˣ)
:
(ZMod.AddAutEquivUnits n).symm a = AddAut.mulLeft a