tensorComm_symm

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

URI: https://scilib.ai/kg/mathlib#QuadraticForm.tensorComm_symm

English

The symmetry of tensorComm: (tensorComm Q1 Q2).symm = tensorComm Q2 Q1.

Русский

Симметрия tensorComm: (tensorComm Q1 Q2).symm = tensorComm Q2 Q1.

LaTeX

$$$\\text{tensorComm}_{{symm}} (Q_1) (Q_2) = \\text{tensorComm} (Q_2) (Q_1)$$$

Lean4

@[simp]
theorem tensorComm_symm (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) :
    (tensorComm Q₁ Q₂).symm = tensorComm Q₂ Q₁ :=
  rfl

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

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

Разделы

Аффилиация

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