comm_symm — Mathlib

English

The swap isomorphism switches the two tensor factors, so it maps a ⊗ b to b ⊗ a and conversely the inverse sends b ⊗ a to a ⊗ b.

Русский

Обменная изоморфия меняет местами два множителя в тензорном произведении: a ⊗ b ↦ b ⊗ a, а её обратная карта — обратно.

LaTeX

$$$ (\\mathrm{comm}_{R} A B) (a \\otimes b) = b \\otimes a $$$

Lean4

theorem comm_symm : (TensorProduct.comm R A B).symm = TensorProduct.comm R B A := by ext; rfl

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