Commit 2022-11-06 11:48 34fb08a7

chore(data/finsupp): move and rename finsupp.single_apply_left (#17357) This lemma was known as basis.finsupp.single_apply_left and lived in linear_algebra/basis.lean but it doesn't have anything to do with a basis, so we rename it to just finsupp.single_apply_left and move it to a file with less dependencies.