English
There is a heterobasic version of TensorProduct.uncurry providing a linear map M ⊗R N →A P from a bilinear map M →A N →R P.
Русский
Существует гетеробазовая версия TensorProduct.uncurry, задающая линейное отображение M ⊗R N →A P из билинейного отображения M →A N →R P.
LaTeX
$$$\text{uncurry} : (M \to_A N \to_R P) \to_B M \otimes_R N \to_A P$$$
Lean4
/-- Heterobasic version of `TensorProduct.mk`:
The canonical bilinear map `M →[A] N →[R] M ⊗[R] N`. -/
@[simps! apply]
nonrec def mk (A M N : Type*) [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [SMulCommClass R A M]
[AddCommMonoid N] [Module R N] : M →ₗ[A] N →ₗ[R] M ⊗[R] N :=
{ mk R M N with map_smul' := fun _ _ => rfl }