Lemmas about units in ZMod.

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

• ZMod.unitsMap hm = Units.map ↑(ZMod.castHom hm (ZMod n))

theorem ZMod.unitsMap_def {n m : ℕ} (hm : n ∣ m) : ZMod.unitsMap hm = Units.map ↑(ZMod.castHom hm (ZMod n))

theorem ZMod.unitsMap_comp {n m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) : (ZMod.unitsMap hm).comp (ZMod.unitsMap hd) = ZMod.unitsMap ⋯

@[simp]

theorem ZMod.unitsMap_self (n : ℕ) : ZMod.unitsMap ⋯ = MonoidHom.id (ZMod n)ˣ

theorem ZMod.unitsMap_val {n m : ℕ} (h : n ∣ m) (a : (ZMod m)ˣ) : ↑((ZMod.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) : Function.Surjective ⇑(ZMod.unitsMap h)

theorem ZMod.not_isUnit_of_mem_primeFactors {n p : ℕ} (h : p ∈ n.primeFactors) : ¬IsUnit ↑p

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.