English
Let R be a nonassociative semiring and f a compatible family of ring homomorphisms R → ZMod(p^k). Then the limit map limNthHom f_compat preserves multiplication: limNthHom f_compat (r · s) = limNthHom f_compat r · limNthHom f_compat s for all r, s ∈ R.
Русский
Пусть R — полугруппа без ассоциативности, и имеется совместимый набор гомоморфизмов f_k: R → Z/(p^k). Тогда предел limNthHom f_compat сохраняет умножение: limNthHom f_compat (r·s) = limNthHom f_compat r · limNthHom f_compat s для всех элементов r, s ∈ R.
LaTeX
$$$\\limNthHom f_{\\text{compat}}(r \\cdot s) = \\limNthHom f_{\\text{compat}}(r) \\cdot \\limNthHom f_{\\text{compat}}(s) $$$
Lean4
theorem limNthHom_mul (r s : R) : limNthHom f_compat (r * s) = limNthHom f_compat r * limNthHom f_compat s :=
Subtype.ext <|
Quot.sound <|
nthHomSeq_mul f_compat _
_
-- TODO: generalize this to arbitrary complete discrete valuation rings
