mathlib3

c4c6cd81 - feat(linear_algebra/finsupp): linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M` (#7472)

feat(linear_algebra/finsupp): linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M` (#7472) This PR extends the equivalence `finsupp.finsupp_prod_equiv` to a linear equivalence (to be used in the `bundled-basis` refactor).