map_finsupp_linearCombination — Mathlib

English

If f: M → N is linear and (g : ι → M) with l ∈ ι →₀ R is a finitely supported family of coefficients, then applying f to the linear combination of g with l equals the linear combination of f∘g with l.

Русский

Если f: M → N линейно и имеется семейство g : ι → M с коэффициентами l ∈ ι →₀ R, то применение f к линейной комбинации g с весами l равно линейной комбинации f∘g с тем же набором весов.

LaTeX

$$$f\left(\operatorname{linearCombination}_R\ g\ l\right) = \operatorname{linearCombination}_R\ (f\circ g)\ l$$$

Lean4

theorem map_finsupp_linearCombination (f : M →ₗ[R] N) {ι : Type*} {g : ι → M} (l : ι →₀ R) :
    f (linearCombination R g l) = linearCombination R (f ∘ g) l :=
  apply_linearCombination _ _ _ _

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