instMonoidal

Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.monoidalOfHasFiniteProducts.instMonoidal

Lean4

/-- Promote a functor that preserves finite products to a monoidal functor between
categories equipped with the monoidal category structure given by finite products. -/
instance : F.Monoidal :=
  .ofOplaxMonoidal F

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

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

Разделы

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

Аффилиация

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