leftComm_tmul

Mathlib.RingTheory.TensorProduct.Basic

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

English

The tmul action respects the leftComm isomorphism on tmul: leftComm (m ⊗ₜ (n ⊗ₜ p)) = n ⊗ₜ (m ⊗ₜ p).

Русский

Действие TMul сохраняет лево-перестановку: leftComm (m ⊗ (n ⊗ p)) = n ⊗ (m ⊗ p).

LaTeX

$$leftComm_R A B C (m ⊗ₜ (n ⊗ₜ p)) = n ⊗ₜ (m ⊗ₜ p)$$

Lean4

@[simp]
theorem leftComm_tmul (m : A) (n : B) (p : C) : leftComm R A B C (m ⊗ₜ (n ⊗ₜ p)) = n ⊗ₜ (m ⊗ₜ p) :=
  rfl

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

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

Разделы

Аффилиация

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