English
There is a canonical ring homomorphism ZMod n →+* R with toFun = cast, whenever m divides n.
Русский
Существует канонический гомоморфизм колец ZMod n →+* R, которому сопоставляется отображение toFun = cast, при m | n.
LaTeX
$$$\\\\exists \\\\phi : ZMod n \\\\to+* R, \\\\text{toFun} = \\\\operatorname{cast} \\\\land \\\\text{map_zero}' \\\\land \\\\text{map_one}' \\\\land \\\\text{map_add}' \\\\land \\\\text{map_mul}'$$$
Lean4
/-- The canonical ring homomorphism from `ZMod n` to a ring of characteristic dividing `n`.
See also `ZMod.lift` for a generalized version working in `AddGroup`s.
-/
def castHom (h : m ∣ n) (R : Type*) [Ring R] [CharP R m] : ZMod n →+* R
where
toFun := cast
map_zero' := cast_zero
map_one' := cast_one h
map_add' := cast_add h
map_mul' := cast_mul h
