Commit 2021-02-05 15:46 c2c686e4

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