assoc_tmul — Mathlib

English

On simple tensors the heterobasic associator respects associativity: (m ⊗ p) ⊗ q maps to m ⊗ (p ⊗ q).

Русский

На простых тензорах гетеробазовая ассоциаторная карта сохраняет ассоциативность: (m ⊗ p) ⊗ q ↦ m ⊗ (p ⊗ q).

LaTeX

$$$\text{assoc}_{R,A,B,M,P,Q}((m\otimes_A p)\otimes_R q) = m\otimes_A (p\otimes_R q)$$$

Lean4

@[simp]
theorem assoc_tmul (m : M) (p : P) (q : Q) : assoc R A B M P Q ((m ⊗ₜ p) ⊗ₜ q) = m ⊗ₜ (p ⊗ₜ q) :=
  rfl

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