assoc_symm_tmul — Mathlib

English

The associator sends a pure tensor to the corresponding rebracketed pure tensor: (m ⊗ n ⊗ p) maps to m ⊗ (n ⊗ p).

Русский

Ассоциатор переводит чистый тензор между скобками: (m ⊗ n ⊗ p) → m ⊗ (n ⊗ p).

LaTeX

$$$\\big(\\text{assoc}_R(M,N,P)\\big)(m\\otimes_R n\\otimes_R p) = m\\otimes_R (n\\otimes_R p)$$$

Lean4

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

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