English
There is a linear equivalence between multilinear maps on a sum index and maps that curry to a pair of multilinear maps on the components.
Русский
Существует линейное эквивалентное отображение между много-линейными отображениями на сумму индексов и отображениями, которые каррируют к паре много-линейных отображений по компонентам.
LaTeX
$$$\\text{currySumEquiv}: \\operatorname{MultilinearMap} R N M_2 \\simeq_L \\operatorname{MultilinearMap} R (\\lambda i. N(\\mathrm{inl}\, i)) (\\operatorname{MultilinearMap} R (\\lambda i. N(\\mathrm{inr}\, i)) M_2)$$$
Lean4
@[simp]
theorem currySum_apply' {N : Type*} [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun _ : ι ⊕ ι' ↦ N) M₂)
(u : ι → N) (v : ι' → N) : currySum f u v = f (Sum.elim u v) :=
rfl
