Documentation

Mathlib.Data.ZMod.Aut

Automorphism Group of ZMod. #

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