mathlib

9aed6c94 - feat(data/finsupp,linear_algebra): `finsupp.split` is an equivalence (#7490)

feat(data/finsupp,linear_algebra): `finsupp.split` is an equivalence (#7490) This PR shows that for finite types `η`, `finsupp.split` is an equivalence between `(Σ (j : η), ιs j) →₀ α` and `Π j, (ιs j →₀ α)`. To be used in the `bundled-basis` refactor Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>