rightComm_tmul — Mathlib

English

There is a canonical linear equivalence M ⊗ N ⊗ (P ⊗ Q) ≅ M ⊗ P ⊗ (N ⊗ Q) that rearranges the factors pairwise.

Русский

Существует канонический линейный эквивалент между M ⊗ N ⊗ (P ⊗ Q) и M ⊗ P ⊗ (N ⊗ Q), переставляющий фактори по парам.

LaTeX

$$$\\text{tensorTensorTensorComm}_R^{M,N,P,Q} : M\\otimes_R N \\otimes_R (P\\otimes_R Q) \\cong_R M\\otimes_R P \\otimes_R (N\\otimes_R Q)$$$

Lean4

@[simp]
theorem rightComm_tmul (m : M) (n : N) (p : P) : rightComm R M N P ((m ⊗ₜ n) ⊗ₜ p) = (m ⊗ₜ p) ⊗ₜ n :=
  rfl

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