mapBilinear — Mathlib

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

Похожие утверждения