assoc_tmul — Mathlib

English

The associator respects simple tensors: assoc R S A C D ((x ⊗_S y) ⊗_R z) = x ⊗_S (y ⊗_R z).

Русский

Ассоциатор сохраняет простой тензор: ассоциатор примененный к ((x ⊗_S y) ⊗_R z) равен x ⊗_S (y ⊗_R z).

LaTeX

$$$\text{assoc}_{R,S,A,C,D}((x \otimes_S y) \otimes_R z) = x \otimes_S (y \otimes_R z)$$$

Lean4

@[simp]
theorem assoc_tmul (x : A) (y : C) (z : D) : Bialgebra.TensorProduct.assoc R S A C D ((x ⊗ₜ y) ⊗ₜ z) = x ⊗ₜ (y ⊗ₜ z) :=
  rfl

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