functorCategoryEquivalenceFunctorMonoidal

Mathlib.CategoryTheory.Action.Monoidal

URI: https://scilib.ai/kg/mathlib#Action.functorCategoryEquivalenceFunctorMonoidal

← MathLib Explorer

English

Same as above: the functor in the equivalence is monoidal.

Русский

То же самое: функтор в эквивалентности является моноидальным.

LaTeX

$$$\text{Monoidal}(\mathrm{FunctorCategoryEquivalence.functorMonoidal})$$$

Lean4

instance functorCategoryEquivalenceFunctorMonoidal : (functorCategoryEquivalence V G).functor.Monoidal := by
  dsimp only [functorCategoryEquivalence_functor]; infer_instance

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

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

Разделы

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

Аффилиация

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