English
There is a linear equivalence lift.equiv between bilinear maps and maps M ⊗ N → P that respects the canonical identifications.
Русский
Существует линейное эквивалентное соответствие lift.equiv между билинейными отображениями и отображениями M ⊗ N → P с сохранением канонических идентификаций.
LaTeX
$$$\\mathrm{lift\\,equiv} : (M \\to_\\ell[R] N \\to_\\ell[R] P) \\cong_\\ell[R] M ⊗[R] N \\to_\\ell[R] P.$$$
Lean4
/-- Linearly constructing a linear map `M ⊗ N → P` given a bilinear map `M → N → P`
with the property that its composition with the canonical bilinear map `M → N → M ⊗ N` is
the given bilinear map `M → N → P`. -/
def uncurry : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] P
where
toFun := lift
map_add' f g := by ext; rfl
map_smul' _ _ := by ext; rfl
