English
lift f_compat is the canonical p-adic limit map from R to ℤ_[p], and it coincides with the limit limNthHom f_compat: lift f_compat = limNthHom f_compat.
Русский
lift f_compat является каноническим пределом в p-адических числах ℤ_[p] от кольца R, и совпадает с пределом limNthHom f_compat: lift f_compat = limNthHom f_compat.
LaTeX
$$$\\text{lift} \\, f_{\\text{compat}} = \\limNthHom f_{\\text{compat}}$$$
Lean4
/-- `lift f_compat` is the limit of a sequence `f` of compatible ring homs `R →+* ZMod (p^k)`,
with the equality `lift f_compat r = PadicInt.limNthHom f_compat r`.
-/
def lift : R →+* ℤ_[p] where
toFun := limNthHom f_compat
map_one' := limNthHom_one f_compat
map_mul' := limNthHom_mul f_compat
map_zero' := limNthHom_zero f_compat
map_add' := limNthHom_add f_compat
