tensorTensorTensorComm_tmul — Mathlib

English

On simple tensors, rightComm acts by swapping the inner two factors.

Русский

На простых тензорах rightComm меняет местами внутренние два фактора.

LaTeX

$$$\text{rightComm}_{R S B M P Q}( (m \otimes p) \otimes q ) = (m \otimes q) \otimes p$$$

Lean4

@[simp]
theorem tensorTensorTensorComm_tmul (m : M) (n : N) (p : P) (q : Q) :
    tensorTensorTensorComm R S A B M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q) :=
  rfl

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