mathlib

34fb08a7 - chore(data/finsupp): move and rename `finsupp.single_apply_left` (#17357)

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.