mapBilinear — Mathlib

English

Scaling on the right commutes with tensor-product mapping: map f (r • g) = r • map f g.

Русский

Умножение справа на отображение совместимо с отображением тензорного произведения: map f (r • g) = r • map f g.

LaTeX

$$$\\operatorname{map}(f, r \\cdot g) = r \\cdot \\operatorname{map}(f, g)$$$

Lean4

/-- The tensor product of a pair of linear maps between modules, bilinear in both maps. -/
def mapBilinear : (M →ₗ[R] P) →ₗ[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q :=
  LinearMap.mk₂ R map map_add_left map_smul_left map_add_right map_smul_right

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