assoc_tmul — Mathlib

English

The associator is defined as a canonical linear isomorphism between M ⊗R N ⊗R P and M ⊗R (N ⊗R P).

Русский

Ассоциатор задаётся как канонический линейный изоморфизм между M ⊗R N ⊗R P и M ⊗R (N ⊗R P).

LaTeX

$$$\\text{assoc}_R(M,N,P) : M\\otimes_R N\\otimes_R P \\cong_R M\\otimes_R (N\\otimes_R P)$$$

Lean4

@[simp]
theorem assoc_tmul (m : M) (n : N) (p : P) : (TensorProduct.assoc R M N P) (m ⊗ₜ n ⊗ₜ p) = m ⊗ₜ (n ⊗ₜ p) :=
  rfl

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