mathlib

71bb9f23 - chore(linear_algebra/finsupp): Implement lsingle in terms of single_add_hom (#4605)