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
    theorem ZMod.unitsMap_surjective {n : } {m : } [hm : NeZero m] (h : n m) :
    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.