tensorObj

Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

URI: https://scilib.ai/kg/mathlib#AugmentedSimplexCategory.tensorObj

Lean4

/-- The tensor product of two objects of `AugmentedSimplexCategory`. -/
def tensorObj (m n : AugmentedSimplexCategory) : AugmentedSimplexCategory :=
  match m, n with
  | .of m, .of n => .of <| tensorObjOf m n
  | .star, x => x
  | x, .star => x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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