English
LinearEquiv.curry provides a linear equivalence between functions of two variables and functions of one variable returning functions, with uncurry as inverse.
Русский
LinearEquiv.curry задаёт линейное эквивалентное соответствие между функциями двух переменных и функций одной переменной, возвращающих функции, с uncurry как обратной.
LaTeX
$$$$ \\text{LinearEquiv.curry} : (V \\times V_2 \\to M) \\simeq_ℝ (V \\to V_2 \\to M) $$$$
Lean4
/-- Linear equivalence between a curried and uncurried function.
Differs from `TensorProduct.curry`. -/
protected def curry : (V × V₂ → M) ≃ₗ[R] V → V₂ → M :=
{ Equiv.curry _ _ _ with
map_add' := fun _ _ ↦ rfl
map_smul' := fun _ _ ↦ rfl }
