Commit 2025-03-08 10:36 d2a9987b
View on Github →feat(LinearAlgebra/Finsupp/linearCombination): add bilinearCombination (#22678)
Add Finsupp.bilinearCombination
and Fintype.bilinearCombination
as bilinear maps.
Previously, Fintype.linearCombination
was a bilinear map, but Finsupp.linearCombination
was only linear in the second variable.
That made Fintype.linearCombination
unusable in the noncommutative case.
By consistency, Fintype.linearCombination
is downgraded to a linear map.