sum_smul_index_addMonoidHom — Mathlib

English

For g : α →₀ M, b ∈ R and h : α → M →+ N, we have ((b • g).sum h) = g.sum (λ i c, h i (b • c)).

Русский

Для g : α →₀ M, b ∈ R и h : α → M →+ N, выполняется ((b • g).sum h) = g.sum (λ i c, h i (b • c)).

LaTeX

$$$[AddZeroClass M][AddCommMonoid N][SMulZeroClass R M] {g : α \\to_0 M} {b : R}{h : α → M →+ N} : ((b • g).sum h) = g.sum (\\lambda i c, h i (b • c))$$$

Lean4

/-- A version of `Finsupp.sum_smul_index'` for bundled additive maps. -/
theorem sum_smul_index_addMonoidHom [AddZeroClass M] [AddCommMonoid N] [SMulZeroClass R M] {g : α →₀ M} {b : R}
    {h : α → M →+ N} : ((b • g).sum fun a => h a) = g.sum fun i c => h i (b • c) :=
  sum_mapRange_index fun i => (h i).map_zero

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