leftAssocTensor_obj — Mathlib

English

The left-associated triple tensor functor sends a triple to the left-associated tensor: X ↦ (X1 ⊗ X2.1) ⊗ X2.2.

Русский

Лево-ассоциированный тройной тензор-функтор отправляет тройку в левостороннее тензорное произведение.

LaTeX

$$(LeftAssocTensor C).obj X = (X.1 ⊗ X.2.1) ⊗ X.2.2$$

Lean4

@[simp]
theorem leftAssocTensor_obj (X) : (leftAssocTensor C).obj X = (X.1 ⊗ X.2.1) ⊗ X.2.2 :=
  rfl

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