Documentation

Mathlib.Data.ZMod.Aut

Automorphism Group of ZMod. #

source
๐Ÿ”ธ coverage
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.

Instances For
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem ZMod.AddAutEquivUnits_symm_apply (n : โ„•) (a : (ZMod n)หฃ) :
    (AddAutEquivUnits n).symm a = AddAut.mulLeft a
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem ZMod.AddAutEquivUnits_apply (n : โ„•) (f : AddAut (ZMod n)) :
    (AddAutEquivUnits n) f = Units.mkOfMulEqOne (f 1) (fโปยน 1) โ‹ฏ