English
There is a canonical bilinear map associated to any linear map on a tensor product; its curry is the bilinear map M × N → P given by pairing an M-element with an N-element and applying f to their simple tensor.
Русский
Существует каноническое билинейное отображение, связанное с любым линейным отображением на тензорном произведении; его карри — билинейное отображение M × N → P, заданное парой элементов и применением f к их простому тензору.
LaTeX
$$$\\text{curry} : (M \\otimes_R N \\to P) \\to (M \\to_R N \\to_R P)$, \\quad $(\\text{curry}(f))(m)(n) = f(m \\otimes n).$$$
Lean4
/-- Given a linear map `M ⊗ N → P`, compose it with the canonical bilinear map `M → N → M ⊗ N` to
form a bilinear map `M → N → P`. -/
def curry (f : M ⊗[R] N →ₗ[R] P) : M →ₗ[R] N →ₗ[R] P :=
lcurry R M N P f
