sectionsMonoid

Mathlib.Algebra.Category.MonCat.Limits

URI: https://scilib.ai/kg/mathlib#MonCat.sectionsMonoid

English

The sections Monoid is the monoid structure on the flat sections induced by sectionsSubmonoid.

Русский

Моноид секций дается моноидальной структурой плоских секций, порожденной sectionsSubmonoid.

LaTeX

$$$\text{sections Monoid}(F) = (\text{sections Submonoid}(F)).toMonoid$$$

Lean4

@[to_additive]
instance sectionsMonoid : Monoid (F ⋙ forget MonCat.{u}).sections :=
  (sectionsSubmonoid F).toMonoid

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

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

Разделы

Аффилиация

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