map_dfinsuppSumAddHom — Mathlib

English

Linear maps respect the additive-sum construction given by sumAddHom.

Русский

Линейные отображения сохраняют операцию суммирования в sumAddHom.

LaTeX

$$f (sumAddHom g t) = sumAddHom (fun i => f.toAddMonoidHom.comp (g i)) t$$

Lean4

@[simp]
theorem map_dfinsuppSumAddHom (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ i, γ i} {g : ∀ i, γ i →+ M} :
    f (sumAddHom g t) = sumAddHom (fun i => f.toAddMonoidHom.comp (g i)) t :=
  f.toAddMonoidHom.map_dfinsuppSumAddHom _ _

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