Documentation

Mathlib.Data.ZMod.Units

Lemmas about units in ZMod. #

source
def ZMod.unitsMap {n : ℕ} {m : ℕ} (hm : n ∣ m) :
(ZMod m)ˣ →* (ZMod n)ˣ

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

Equations
Instances For
    source
    theorem ZMod.unitsMap_def {n : ℕ} {m : ℕ} (hm : n ∣ m) :
    ZMod.unitsMap hm = Units.map ↑(ZMod.castHom hm (ZMod n))
    source
    theorem ZMod.unitsMap_comp {n : ℕ} {m : ℕ} {d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
    MonoidHom.comp (ZMod.unitsMap hm) (ZMod.unitsMap hd) = ZMod.unitsMap ⋯
    source
    @[simp]
    theorem ZMod.unitsMap_self (n : ℕ) :
    ZMod.unitsMap ⋯ = MonoidHom.id (ZMod n)ˣ
    source
    theorem ZMod.IsUnit_cast_of_dvd {n : ℕ} {m : ℕ} (hm : n ∣ m) (a : (ZMod m)ˣ) :
    IsUnit (ZMod.cast ↑a)
    source
    theorem ZMod.unitsMap_surjective {n : ℕ} {m : ℕ} [hm : NeZero m] (h : n ∣ m) :
    Function.Surjective ⇑(ZMod.unitsMap h)
    source
    theorem ZMod.not_isUnit_of_mem_primeFactors {n : ℕ} {p : ℕ} (h : p ∈ n.primeFactors) :
    ¬IsUnit ↑p
    source
    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.