English
There is a heterobasic version of homTensorHomMap: homTensorHomMap : ((M →_A P) ⊗_R (N →_R Q)) →_B (M ⊗_R N →_A P ⊗_R Q).
Русский
Существет гетеробазовая версия homTensorHomMap: homTensorHomMap : ((M →_A P) ⊗_R (N →_R Q)) →_B (M ⊗_R N →_A P ⊗_R Q).
LaTeX
$$$\mathrm{homTensorHomMap} : ((M \to_A P) \otimes_R (N \to_R Q)) \to_B (M \otimes_R N \to_A P \otimes_R Q)$$$
Lean4
/-- Heterobasic version of `TensorProduct.map_bilinear` -/
def mapBilinear : (M →ₗ[A] P) →ₗ[B] (N →ₗ[R] Q) →ₗ[R] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) :=
LinearMap.mk₂' _ _ map map_add_left map_smul_left map_add_right map_smul_right