English
A more bundled version of domCoprod that maps ((ι1 → N) → N1) ⊗ ((ι2 → N) → N2) to (ι1 ⊕ ι2 → N) → N1 ⊗ N2.
Русский
Упакованная версия domCoprod: ((ι1 → N) → N1) ⊗ ((ι2 → N) → N2) → (ι1 ⊕ ι2 → N) → N1 ⊗ N2.
LaTeX
$$$domCoprod' : (\mathrm{MultilinearMap}\,R (\lambda _ : ι_1. N) N_1) \otimes_R (\mathrm{MultilinearMap}\,R (\lambda _ : ι_2. N) N_2) \to_L_R \mathrm{MultilinearMap}\,R (\lambda _ : ι_1 ⊕ ι_2. N) (N_1 ⊗_R N_2).$$$
Lean4
/-- A more bundled version of `MultilinearMap.domCoprod` that maps
`((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂)` to `(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂`. -/
def domCoprod' :
MultilinearMap R (fun _ : ι₁ => N) N₁ ⊗[R] MultilinearMap R (fun _ : ι₂ => N) N₂ →ₗ[R]
MultilinearMap R (fun _ : ι₁ ⊕ ι₂ => N) (N₁ ⊗[R] N₂) :=
domCoprodDep' (R := R) (N := fun (_ : ι₁ ⊕ ι₂) ↦ N)
