English
The two-step process of curryRight then uncurryRight is the identity on multilinear maps.
Русский
Два шага: curryRight затем uncurryRight — тождество на много-линейных отображениях.
LaTeX
$$$$f.uncurryRight.curryRight = f.$$$$
Lean4
/-- Given a multilinear map `f` in `n+1` variables, split the last variable to obtain
a multilinear map in `n` variables taking values in linear maps from `M (last n)` to `M₂`, given by
`m ↦ (x ↦ f (snoc m x))`. -/
def curryRight (f : MultilinearMap R M M₂) :
MultilinearMap R (fun i : Fin n => M (Fin.castSucc i)) (M (last n) →ₗ[R] M₂) :=
MultilinearMap.mk' fun m ↦
{ toFun := fun x => f (snoc m x)
map_add' := fun x y => by simp_rw [f.snoc_add]
map_smul' := fun c x => by simp only [f.snoc_smul, RingHom.id_apply] }
