mulMap_comm — Mathlib

English

The product map is symmetric up to the natural commutativity isomorphism of the tensor product: mulMap B A equals mulMap A B composed with the commutativity map.

Русский

Произведение мап симметрично относительно естественного изоморфизма коммутативности тензорного произведения: mulMap B A = mulMap A B ∘ TensorProduct.comm.

LaTeX

$$$\text{mulMap } B A = (\text{mulMap } A B) \circ (\text{Algebra.TensorProduct.comm } R B A)$$$

Lean4

theorem mulMap_comm : mulMap B A = (mulMap A B).comp (Algebra.TensorProduct.comm R B A) := by ext <;> simp

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