Automorphism Group of ZMod.

def ZMod.AddAutEquivUnits (n : Nat) : MulEquiv (AddAut (ZMod n)) (Units (ZMod n))

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

Equations

• One or more equations did not get rendered due to their size.

theorem ZMod.AddAutEquivUnits_apply (n : Nat) (f : AddAut (ZMod n)) : Eq (DFunLike.coe (AddAutEquivUnits n) f) (Units.mkOfMulEqOne (DFunLike.coe f 1) (DFunLike.coe (Inv.inv f) 1) ⋯)

theorem ZMod.AddAutEquivUnits_symm_apply (n : Nat) (a : Units (ZMod n)) : Eq (DFunLike.coe (AddAutEquivUnits n).symm a) (DFunLike.coe AddAut.mulLeft a)