Given two multilinear maps (ι₁ → N) → N₁ and (ι₂ → N) → N₂, this produces the map (ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂ by taking the coproduct of the domain and the tensor product of the codomain.

This can be thought of as combining equiv.sum_arrow_equiv_prod_arrow.symm with tensor_product.map, noting that the two operations can't be separated as the intermediate result is not a multilinear_map.

While this can be generalized to work for dependent Π i : ι₁, N'₁ i instead of ι₁ → N, doing so introduces sum.elim N'₁ N'₂ types in the result which are difficult to work with and not defeq to the simple case defined here. See this zulip thread.

A more bundled version of multilinear_map.dom_coprod that maps ((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂) to (ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂.