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.unitsMap_val {n m : } (h : n m) (a : (ZMod m)ˣ) :
    ((unitsMap h) a) = (↑a).cast

    unitsMap_val shows that coercing from (ZMod m)ˣ to ZMod n gives the same result when going via (ZMod n)ˣ and ZMod m.

    theorem ZMod.isUnit_cast_of_dvd {n m : } (hm : n m) (a : (ZMod m)ˣ) :
    IsUnit (↑a).cast
    @[deprecated ZMod.isUnit_cast_of_dvd (since := "2024-12-16")]
    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.unitsMap_surjective {n m : } [hm : NeZero m] (h : n m) :
    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.

    theorem ZMod.coe_int_mul_inv_eq_one {n : } {x : } (h : IsCoprime x n) :
    x * (↑x)⁻¹ = 1
    theorem ZMod.coe_int_inv_mul_eq_one {n : } {x : } (h : IsCoprime x n) :
    (↑x)⁻¹ * x = 1
    theorem ZMod.coe_int_mul_val_inv {n : } [NeZero n] {m : } (h : IsCoprime m n) :
    m * (↑m)⁻¹.val = 1
    theorem ZMod.coe_int_val_inv_mul {n : } [NeZero n] {m : } (h : IsCoprime m n) :
    (↑m)⁻¹.val * m = 1
    def ZMod.unitOfIsCoprime {m : } (n : ) (h : IsCoprime n m) :
    (ZMod m)ˣ

    The unit of ZMod m associated with an integer prime to n.

    Equations
    Instances For
      @[simp]
      theorem ZMod.coe_unitOfIsCoprime {m : } (n : ) (h : IsCoprime n m) :
      (unitOfIsCoprime n h) = n
      theorem ZMod.isUnit_inv {m : } {n : } (h : IsUnit n) :