rightComm_symm — Mathlib

English

The symmetry of tensorTensorTensorComm gives an isomorphism in the opposite direction: (tensorTensorTensorComm).symm = tensorTensorTensorComm with swapped roles.

Русский

Симметрия tensorTensorTensorComm задаёт противоположный изоморфизм: (tensorTensorTensorComm).symm соответствует обмену ролями.

LaTeX

$$$\bigl(\text{tensorTensorTensorComm}\;R\;S\;A\;B\;M\;N\;P\;Q\bigr)^{\!-1} = \text{tensorTensorTensorComm}_{R A S B M N P Q}$$$

Lean4

@[simp]
theorem rightComm_symm : (rightComm R S B M P Q).symm = rightComm S R B M Q P :=
  rfl

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