leftComm_tmul

Mathlib.LinearAlgebra.TensorProduct.Tower

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

English

On simple tensors, leftComm acts by swapping the inner two factors: leftComm (m ⊗ (p ⊗ q)) = p ⊗ (m ⊗ q).

Русский

На простых тензорах leftComm преобразует (m ⊗ (p ⊗ q)) в p ⊗ (m ⊗ q).

LaTeX

$$$\text{leftComm}_{R,A,M,P,Q}(m\otimes (p\otimes q)) = p\otimes (m\otimes q)$$$

Lean4

@[simp]
theorem leftComm_tmul (m : M) (p : P) (q : Q) : leftComm R A M P Q (m ⊗ₜ (p ⊗ₜ q)) = p ⊗ₜ (m ⊗ₜ q) :=
  rfl

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

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

Разделы

Аффилиация

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