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) :
    unitsMap hm = Units.map ↑(castHom hm (ZMod n))
    source
    theorem ZMod.unitsMap_comp {n m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
    (unitsMap hm).comp (unitsMap hd) = unitsMap ⋯
    source
    @[simp]
    theorem ZMod.unitsMap_self (n : ℕ) :
    unitsMap ⋯ = MonoidHom.id (ZMod n)ˣ
    source
    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.

    source
    theorem ZMod.isUnit_cast_of_dvd {n m : ℕ} (hm : n ∣ m) (a : (ZMod m)ˣ) :
    IsUnit (↑a).cast
    source
    theorem ZMod.unitsMap_surjective {n m : ℕ} [hm : NeZero m] (h : n ∣ m) :
    Function.Surjective ⇑(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.

    source
    theorem ZMod.intCast_mul_inv_eq_one {n : ℕ} {x : ℤ} (h : IsCoprime x ↑n) :
    ↑x * (↑x)⁻¹ = 1
    source
    @[deprecated ZMod.intCast_mul_inv_eq_one (since := "2026-10-27")]
    theorem ZMod.coe_int_mul_inv_eq_one {n : ℕ} {x : ℤ} (h : IsCoprime x ↑n) :
    ↑x * (↑x)⁻¹ = 1

    Alias of ZMod.intCast_mul_inv_eq_one.

    source
    theorem ZMod.intCast_inv_mul_eq_one {n : ℕ} {x : ℤ} (h : IsCoprime x ↑n) :
    (↑x)⁻¹ * ↑x = 1
    source
    @[deprecated ZMod.intCast_inv_mul_eq_one (since := "2026-10-27")]
    theorem ZMod.coe_int_inv_mul_eq_one {n : ℕ} {x : ℤ} (h : IsCoprime x ↑n) :
    (↑x)⁻¹ * ↑x = 1

    Alias of ZMod.intCast_inv_mul_eq_one.

    source
    theorem ZMod.intCast_mul_val_inv {n : ℕ} [NeZero n] {m : ℤ} (h : IsCoprime m ↑n) :
    ↑m * ↑(↑m)⁻¹.val = 1
    source
    @[deprecated ZMod.intCast_mul_val_inv (since := "2026-10-27")]
    theorem ZMod.coe_int_mul_val_inv {n : ℕ} [NeZero n] {m : ℤ} (h : IsCoprime m ↑n) :
    ↑m * ↑(↑m)⁻¹.val = 1

    Alias of ZMod.intCast_mul_val_inv.

    source
    theorem ZMod.intCast_val_inv_mul {n : ℕ} [NeZero n] {m : ℤ} (h : IsCoprime m ↑n) :
    ↑(↑m)⁻¹.val * ↑m = 1
    source
    @[deprecated ZMod.intCast_val_inv_mul (since := "2026-10-27")]
    theorem ZMod.coe_int_val_inv_mul {n : ℕ} [NeZero n] {m : ℤ} (h : IsCoprime m ↑n) :
    ↑(↑m)⁻¹.val * ↑m = 1

    Alias of ZMod.intCast_val_inv_mul.

    source
    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
      source
      @[simp]
      theorem ZMod.coe_unitOfIsCoprime {m : ℕ} (n : ℤ) (h : IsCoprime n ↑m) :
      ↑(unitOfIsCoprime n h) = ↑n
      source
      theorem ZMod.isUnit_inv {m : ℕ} {n : ℤ} (h : IsUnit ↑n) :
      IsUnit (↑n)⁻¹
      source
      theorem ZMod.isUnit_intCast_iff_isCoprime (n : ℤ) (m : ℕ) :
      IsUnit ↑n ↔ IsCoprime (↑m) n
      source
      @[deprecated ZMod.isUnit_intCast_iff_isCoprime (since := "2026-10-27")]
      theorem ZMod.coe_int_isUnit_iff_isCoprime (n : ℤ) (m : ℕ) :
      IsUnit ↑n ↔ IsCoprime (↑m) n

      Alias of ZMod.isUnit_intCast_iff_isCoprime.

      source
      instance ZMod.instFiniteZModUnits (n : ℕ) :
      Finite (ZMod n)ˣ

      For each n ≥ 0, the unit group of ZMod n is finite.