Commit 2021-05-28 19:12 f74a3753
View on Github →chore(linear_algebra/finsupp): remove useless lemma (#7734) The lemma is not used in mathlib, it's mathematically useless (you'd never have a surjective function from an indexing set to a module), and it's badly named, so I propose removing it entirely.