mathlib

e7b8421e - chore(linear_algebra/finsupp): turn `finsupp.lsum` into `add_equiv` (#4597)