rightComm_symm_tmul — Mathlib

English

On simple tensors, the symm of tensorTensorTensorComm maps (m ⊗ (p ⊗ q)) to (m ⊗ p) ⊗ q in the swapped order of factors.

Русский

На простых тензорах симметрическое отображение tensorTensorTensorComm переводит (m ⊗ (p ⊗ q)) в (m ⊗ p) ⊗ q после перестановки факторов.

LaTeX

$$$(tensorTensorTensorComm R S A B M N P Q)^{-1}((m)\otimes_A(p\otimes_R q)) = (m\otimes_A p)\otimes_R q$$$

Lean4

theorem rightComm_symm_tmul (m : M) (p : P) (q : Q) : (rightComm R S B M P Q).symm ((m ⊗ₜ q) ⊗ₜ p) = (m ⊗ₜ p) ⊗ₜ q :=
  rfl

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