mathlib3

8d9eb266 - chore(linear_algebra/finsupp): make lsum a linear_equiv (#6183)