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)`.





leanprover-community/mathlib,leanprover-community/mathlib