sum_smul_index' — Mathlib

English

A variant of the previous identity for g : α →₀ M and h : α → M → N with h i 0 = 0; (b • g).sum h = g.sum (i, h i (b • c)).

Русский

Вариант предыдущего тождества для g : α →₀ M и h : α → M → N; (b • g).sum h = g.sum (i, h i (b • c)).

LaTeX

$$$[Zero M][SMulZeroClass R M][AddCommMonoid N] {g : α \\to_0 M} {b : R} {h : α → M → N} (h0 : \\forall i, h i 0 = 0) :\n (b \\cdot g).\\mathrm{sum} h = g.\\mathrm{sum} (\\lambda i c, h i (b \\cdot c))$$$

Lean4

theorem sum_smul_index' [Zero M] [SMulZeroClass R M] [AddCommMonoid N] {g : α →₀ M} {b : R} {h : α → M → N}
    (h0 : ∀ i, h i 0 = 0) : (b • g).sum h = g.sum fun i c => h i (b • c) :=
  Finsupp.sum_mapRange_index h0

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