English
Uncurrying on the right recovers the original map after currying on the right.
Русский
Развёртывание справа восстанавливает исходную карту после каррирования справа.
LaTeX
$$$$f.uncurryRight = f$$ after currying right, i.e., f.uncurryRight.curryRight = f.$$
Lean4
/-- Given a multilinear map `f` in `n` variables to the space of linear maps from `M (last n)` to
`M₂`, construct the corresponding multilinear map on `n+1` variables obtained by concatenating
the variables, given by `m ↦ f (init m) (m (last n))` -/
def uncurryRight (f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)) :
MultilinearMap R M M₂ :=
MultilinearMap.mk' (fun m ↦ f (init m) (m (last n))) (fun m i x y ↦ by cases i using Fin.lastCases <;> simp [Ne.symm])
(fun m i c x ↦ by cases i using Fin.lastCases <;> simp [Ne.symm])
