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)