English
The heterobasic lcurry is compatible with composition in a natural way, respecting the bilinear structure.
Русский
Гетеробазовая lcurry совместима с композициями, уважая билинейную структуру.
LaTeX
$$$\text{lcurry}(f \circ g) = \text{lcurry}(f) \circ \text{lcurry}(g)$$$
Lean4
/-- Heterobasic version of `TensorProduct.lcurry`:
Given a linear map `M ⊗[R] N →[A] P`, compose it with the canonical
bilinear map `M →[A] N →[R] M ⊗[R] N` to form a bilinear map `M →[A] N →[R] P`. -/
@[simps]
def lcurry : (M ⊗[R] N →ₗ[A] P) →ₗ[B] M →ₗ[A] N →ₗ[R] P
where
toFun := curry
map_add' _ _ := rfl
map_smul' _ _ := rfl