rightAssocTensor_map — Mathlib

English

The right-associated triple tensor map is f.1 ⊗ f.2.1 ⊗ f.2.2 for a morphism f.

Русский

Право-ассоциированного тройного тензорного отображение действует на компоненты так: f.1 ⊗ f.2.1 ⊗ f.2.2.

LaTeX

$$$ (RightAssocTensor C).map f = f.1 \\otimes f.2.1 \\otimes f.2.2. $$$

Lean4

@[simp]
theorem rightAssocTensor_map {X Y} (f : X ⟶ Y) : (rightAssocTensor C).map f = f.1 ⊗ₘ f.2.1 ⊗ₘ f.2.2 :=
  rfl

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