tensorUnitImpl

Mathlib.CategoryTheory.Dialectica.Monoidal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Dial.tensorUnitImpl

Lean4

/-- The unit for the tensor `X ⊗ Y` in `Dial C`. -/
@[simps]
def tensorUnitImpl : Dial C :=
  { src := ⊤_ _, tgt := ⊤_ _, rel := ⊤ }

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

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

Разделы

Аффилиация

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