feat(linear_algebra/multilinear-tensor): Add `multilinear_map.dom_coprod_pi`

[eric-wieser]

This generalizes multilinear_map.dom_coprod to maps with non-uniform argument types, at the expense of introducing unpleasant sum.elim M N pi-types

---

Zulip thread