mathlib3

c2c686e4 - feat(linear_algebra/multilinear): add more `curry` equivs (#6012)

feat(linear_algebra/multilinear): add more `curry` equivs (#6012) * `multilinear_map (λ i : ι ⊕ ι', E) F` is equivalent to `multilinear_map (λ i : ι, E) (multilinear_map (λ i : ι', E) F)`; * given `s : finset (fin n)`, `s.card = k`, and `sᶜ.card = l`, `multilinear_map (λ i : fin n, E) F` is equivalent to `multilinear_map (λ i : fin k, E) (multilinear_map (λ i : fin l, E) F)`.