finsuppTotal — Mathlib

English

A variant of a linear combination map that takes finitely supported coefficients in I and outputs a vector in M by combining the vectors v_i with coefficients from I.

Русский

Вариант отображения линейной комбинации, принимающий коэффициенты в I и выдающий вектор в M через линейную комбинацию со степенью поддержки.

LaTeX

$$finsuppTotal : (ι →₀ I) →ₗ[R] M, defined by аналогия линейной комбинации векторов v$$

Lean4

/-- A variant of `Finsupp.linearCombination` that takes in vectors valued in `I`. -/
noncomputable def finsuppTotal : (ι →₀ I) →ₗ[R] M :=
  (Finsupp.linearCombination R v).comp (Finsupp.mapRange.linearMap I.subtype)

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