English
Let n be a positive integer and A an additive group. For every hom f from Z to A with f(n) = 0, there exists a unique induced hom from Z/nZ to A such that composing with the natural projection Z → Z/nZ recovers f; equivalently, (ZMod.lift n f) ∘ Int.castAddHom (ZMod n) = f.
Русский
Пусть n — положительное целое число и A — аддитивная группа. Для любой гомоморфизмы f : ℤ → A с условием f(n) = 0 существует единственный индуцированный гомоморфизм из ℤ/nℤ в A, который при композиции с естественным отображением ℤ → ℤ/nℤ возвращает f; то есть (ZMod.lift n f) ∘ Int.castAddHom (ZMod n) = f.
LaTeX
$$$ (ZMod.lift\\ n\\ f) \\circ (Int.castAddHom (ZMod\\ n)) = f $$$
Lean4
@[simp]
theorem lift_comp_castAddHom : (ZMod.lift n f).comp (Int.castAddHom (ZMod n)) = f :=
AddMonoidHom.ext <| lift_castAddHom _ _
