productMap_eq_comp_map — Mathlib

English

The product map factors as the composition of the universal left multiplication with the tensor product map: productMap f g = (lmul' R) ∘ (TensorProduct.map f g).

Русский

ProductMap разложим через композицию: productMap f g = (lmul' R) ∘ (TensorProduct.map f g).

LaTeX

$$productMap f g = (lmul' R) ∘ (TensorProduct.map f g)$$

Lean4

theorem productMap_eq_comp_map : productMap f g = (lmul' R).comp (TensorProduct.map f g) := by ext <;> rfl

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