sum_apply — Mathlib

English

For a finite family of linear maps, the coercion to functions distributes over finite sums, i.e., the sum of the coerced functions equals the coercion of the sum of functions.

Русский

Для конечного набора линейных отображений сумма их функций-образов равна образу суммы функций.

LaTeX

$$$\\left(\\sum_{i\\in t} f_i\\right) = \\sum_{i\\in t} f_i \\quad \\text{as elements of } (M \\to M₂).$$$

Lean4

theorem sum_apply (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) (b : M) : (∑ d ∈ t, f d) b = ∑ d ∈ t, f d b :=
  _root_.map_sum ((AddMonoidHom.eval b).comp toAddMonoidHom') f _

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