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.

Estimated changes