English
Again, the bilinearCombination aligns with linearCombination: bilinearCombination R S v = linearCombination R v.
Русский
Снова bilinearCombination совпадает с linearCombination: bilinearCombination R S v = linearCombination R v.
LaTeX
$$$\\mathrm{bilinearCombination}_R^S v = \\mathrm{linearCombination}_R v$$$
Lean4
/-- `Fintype.bilinearCombination R S 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 bilinearCombination : (α → M) →ₗ[S] (α → R) →ₗ[R] M
where
toFun v := Fintype.linearCombination R v
map_add' u v := by ext; simp [Fintype.linearCombination, Finset.sum_add_distrib, Pi.add_apply, smul_add]
map_smul' r v := by ext; simp [Fintype.linearCombination, Finset.smul_sum, smul_comm]
