English
The composition of the R-linear linearCombination with the inverse of Finsupp.linearEquivFunOnFinite equals the Finite variant Fintype.linearCombination: (linearCombination_R v) ∘ (Finsupp.linearEquivFunOnFinite_R_R α).symm.toLinearMap = Fintype.linearCombination_R v.
Русский
Компоновка линейной комбинации Finsupp через обратную биективность эквивалентности равна варианту Fintype.linearCombination.
LaTeX
$$$\\bigl(\\operatorname{linearCombination}_R v\\bigr) \\circ \\bigl(\\mathrm{Finsupp.linearEquivFunOnFinite}_R^R \\alpha\\bigr)^{-1} = \\operatorname{Fintype.linearCombination}_R v$$$
Lean4
/-- `Finsupp.bilinearCombination R S v f` is the linear combination of vectors in `v` with weights
in `f`, as a bilinear map of `v` and `f`.
In the absence of `SMulCommClass R S M`, use `Finsupp.linearCombination`.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
-/
def bilinearCombination : (α → M) →ₗ[S] (α →₀ R) →ₗ[R] M
where
toFun v := linearCombination R v
map_add' u v := by ext; simp [Pi.add_apply, smul_add]
map_smul' r v := by ext; simp [smul_comm]
