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) : MonoidHom.comp (ZMod.unitsMap hm) (ZMod.unitsMap hd) = ZMod.unitsMap (_ : n ∣ d)

@[simp]

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

theorem ZMod.IsUnit_cast_of_dvd {n : ℕ} {m : ℕ} (hm : n ∣ m) (a : (ZMod m)ˣ) : IsUnit ↑↑a