mathlib3

d7f6bd61 - feat(data/finsupp,linear_algebra/finsupp): `finsupp`s and sum types (#6992)

feat(data/finsupp,linear_algebra/finsupp): `finsupp`s and sum types (#6992) This PR contains a few definitions relating sum types and `finsupp`. The main result is `finsupp.sum_arrow_equiv_prod_arrow`, a `finsupp` version of `equiv.sum_arrow_equiv_prod_arrow`. This is turned into a `linear_equiv` by `finsupp.sum_arrow_lequiv_prod_arrow`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>