English
The bilinear arrangement equals the Finite-equivalent linear combination: (linearCombination R v) ∘ (Finsupp.linearEquivFunOnFinite R R α).symm.toLinearMap equals Fintype.linearCombination R v.
Русский
Билинейная схема равна линейной комбинации для конечного индекса: (linearCombination R v) ∘ (Finsupp.linearEquivFunOnFinite R R α)^{-1} = Fintype.linearCombination R v.
LaTeX
$$$(\\operatorname{linearCombination}_R v) \\circ (\\mathrm{Finsupp.linearEquivFunOnFinite}_R^R \\alpha)^{-1} = \\operatorname{Fintype.linearCombination}_R v$$$
Lean4
/-- `Fintype.linearCombination R v f` is the linear combination of vectors in `v` with weights
in `f`. This variant of `Finsupp.linearCombination` is defined on fintype indexed vectors.
This map is linear in `v` if `R` is commutative, and always linear in `f`.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
-/
protected def linearCombination : (α → R) →ₗ[R] M
where
toFun f := ∑ i, f i • v i
map_add' f g := by simp_rw [← Finset.sum_add_distrib, ← add_smul]; rfl
map_smul' r f := by simp_rw [Finset.smul_sum, smul_smul]; rfl
