English
Define a linear map uncurry that sends a bilinear map to a linear map M ⊗ N → P.
Русский
Определяем линейное отображение uncurry, переходящее билинейное отображение в линейное отображение M ⊗ N → P.
LaTeX
$$$\\text{uncurry} : (M \\to_\\ell[R] N \\to_\\ell[R] P) \\to_\\ell[R] M ⊗[R] N \\to_\\ell[R] P.$$$
Lean4
/-- This used to be an `@[ext]` lemma, but it fails very slowly when the `ext` tactic tries to apply
it in some cases, notably when one wants to show equality of two linear maps. The `@[ext]`
attribute is now added locally where it is needed. Using this as the `@[ext]` lemma instead of
`TensorProduct.ext'` allows `ext` to apply lemmas specific to `M →ₗ _` and `N →ₗ _`.
See note [partially-applied ext lemmas]. -/
theorem ext {g h : M ⊗ N →ₗ[R] P} (H : (mk R M N).compr₂ g = (mk R M N).compr₂ h) : g = h := by
rw [← lift_mk_compr₂ g, H, lift_mk_compr₂]
