English
The symm of curryFinFinset applied to f and a vector m equals a certain evaluation of f with left/right indices split.
Русский
Симметрическое применение curryFinFinset к f и вектору m даёт определённую оценку f с разбиением индексов слева и справа.
LaTeX
$$$ (\\text{curryFinFinset}\\; R\\; M_2\\; M'\\; hk\\; hl)^{\\!-1} f\; m = \\; f(\\text{...}) $$$
Lean4
/-- Multilinear maps on `N : (ι ⊕ ι') → Type*` identify to multilinear maps
from `(fun (i : ι) ↦ N (.inl i))` taking values in the space of
linear maps on `(fun (i : ι') ↦ N (.inr i))`. -/
@[simps]
def currySumEquiv :
MultilinearMap R N M₂ ≃ₗ[R]
MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)
where
toFun := currySum
invFun := uncurrySum
left_inv _ := by simp
map_add' := by aesop
map_smul' := by aesop
