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 ⋯
@[deprecated ZMod.isUnit_cast_of_dvd]
Alias of ZMod.isUnit_cast_of_dvd
.