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) :
    theorem ZMod.isUnit_cast_of_dvd {n m : } (hm : n m) (a : (ZMod m)ˣ) :
    IsUnit (↑a).cast
    @[deprecated ZMod.isUnit_cast_of_dvd]
    theorem ZMod.IsUnit_cast_of_dvd {n m : } (hm : n m) (a : (ZMod m)ˣ) :
    IsUnit (↑a).cast

    Alias of ZMod.isUnit_cast_of_dvd.

    theorem ZMod.not_isUnit_of_mem_primeFactors {n p : } (h : p n.primeFactors) :
    theorem ZMod.eq_unit_mul_divisor {N : } (a : ZMod N) :
    ∃ (d : ), d N ∃ (u : ZMod N), IsUnit u a = u * d

    Any element of ZMod N has the form u * d where u is a unit and d is a divisor of N.