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.