tensorTensorTensorAssoc_symm_tmul

English

A natural associator for a higher-level tensor product: M ⊗ N ⊗ (P ⊗ Q) ≅ M ⊗ (N ⊗ P) ⊗ Q.

Русский

Естественный ассоциатор для более сложного тензорного произведения: M ⊗ N ⊗ (P ⊗ Q) ≅ M ⊗ (N ⊗ P) ⊗ Q.

LaTeX

$$$M \\otimes_R N \\otimes_R (P \\otimes_R Q) \\cong_R M \\otimes_R (N \\otimes_R P) \\otimes_R Q$$$

Lean4

@[simp]
theorem tensorTensorTensorAssoc_symm_tmul (m : M) (n : N) (p : P) (q : Q) :
    (tensorTensorTensorAssoc R M N P Q).symm (m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q) = m ⊗ₜ n ⊗ₜ (p ⊗ₜ q) :=
  rfl

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