coe_dfinsuppSumAddHom — Mathlib

English

The coercion of sumAddHom g f equals the sumAddHom of the composed maps; that is, the function obtained by viewing sumAddHom g f as a function equals the sumAddHom of the composed g_i functions.

Русский

Пределение суммы sumAddHom g f как функции совпадает с суммой, полученной от композиции соответствующих гомоморфизмов g_i.

LaTeX

$$$ \mathrm{coe}\bigl(\mathrm{sumAddHom}\, g\, f\bigr) = \mathrm{sumAddHom}\bigl(\lambda i. (\mathrm{coeFn}\, R\, S) \circ (g i)\bigr) f $$$

Lean4

@[simp, norm_cast]
theorem coe_dfinsuppSumAddHom [AddZeroClass R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)] (f : Π₀ i, β i)
    (g : ∀ i, β i →+ R →+ S) : ⇑(sumAddHom g f) = sumAddHom (fun i => (coeFn R S).comp (g i)) f :=
  map_dfinsuppSumAddHom (coeFn R S) f g

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