tensorTensorTensorComm_symm

Mathlib.LinearAlgebra.TensorProduct.Tower

URI: https://scilib.ai/kg/mathlib#TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm

English

Symmetry of rightComm matches the swapped version: (rightComm).symm = rightComm with swapped inputs.

Русский

Симметрия rightComm совпадает с версией после перестановки входов.

LaTeX

$$$\text{rightComm}_{R S B M P Q}^{-1} = \text{rightComm}_{S R B M Q P}$$$

Lean4

@[simp]
theorem tensorTensorTensorComm_symm :
    (tensorTensorTensorComm R S A B M N P Q).symm = tensorTensorTensorComm R A S B M P N Q :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru