tensor_right'

Mathlib.Tactic.CategoryTheory.MonoidalComp

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCoherence.tensor_right'

Lean4

@[simps]
instance tensor_right' (X Y : C) [MonoidalCoherence Y (𝟙_ C)] : MonoidalCoherence (X ⊗ Y) X :=
  ⟨whiskerLeftIso X ⊗𝟙 ≪≫ (ρ_ X)⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru