English
If n divides m, there is a natural group homomorphism from units of ZMod m to units of ZMod n, given by reduction modulo n along the divisor.
Русский
Если n делит m, существует естественный гомоморфизм между группами единиц ZMod m и ZMod n, задаваемый редукцией по mod n.
LaTeX
$$$$ \\mathrm{unitsMap}_{n,m}(hm) : (\\mathbb{Z}/m\\mathbb{Z})^{\\times} \\to (\\mathbb{Z}/n\\mathbb{Z})^{\\times}. $$$$
Lean4
/-- `unitsMap` is a group homomorphism that maps units of `ZMod m` to units of `ZMod n` when `n`
divides `m`. -/
def unitsMap (hm : n ∣ m) : (ZMod m)ˣ →* (ZMod n)ˣ :=
Units.map (castHom hm (ZMod n))
