tensorTensorTensorComm_tmul — Mathlib

English

Applying the left-commutativity isomorphism to m ⊗ (n ⊗ p) yields n ⊗ (m ⊗ p).

Русский

Применение лево-симметрии к m ⊗ (n ⊗ p) даёт n ⊗ (m ⊗ p).

LaTeX

$$$\\text{leftComm}\\; (m\\otimes_R (n\\otimes_R p)) = n \\otimes_R (m\\otimes_R p)$$$

Lean4

@[simp]
theorem tensorTensorTensorComm_tmul (m : M) (n : N) (p : P) (q : Q) :
    tensorTensorTensorComm R M N P Q (m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ p ⊗ₜ (n ⊗ₜ q) :=
  rfl

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