limNthHom_add — Mathlib

English

limNthHom respects addition: limNthHom f_compat (r+s) = limNthHom f_compat r + limNthHom f_compat s.

Русский

limNthHom сохраняет сложение: limNthHom f_compat (r+s) = limNthHom f_compat r + limNthHom f_compat s.

LaTeX

$$limNthHom f_compat (r + s) = limNthHom f_compat r + limNthHom f_compat s$$

Lean4

theorem limNthHom_add (r s : R) : limNthHom f_compat (r + s) = limNthHom f_compat r + limNthHom f_compat s :=
  Subtype.ext <| Quot.sound <| nthHomSeq_add f_compat _ _

Похожие утверждения