Documentation

Mathlib.Data.ZMod.Units

Lemmas about units in ZMod. #

def ZMod.unitsMap {n : } {m : } (hm : n m) :

unitsMap is a group homomorphism that maps units of ZMod m to units of ZMod n when n divides m.

Equations
Instances For
    theorem ZMod.unitsMap_def {n : } {m : } (hm : n m) :
    theorem ZMod.unitsMap_comp {n : } {m : } {d : } (hm : n m) (hd : m d) :
    @[simp]
    theorem ZMod.IsUnit_cast_of_dvd {n : } {m : } (hm : n m) (a : (ZMod m)ˣ) :
    IsUnit a