instMonoidColex

Mathlib.Algebra.Order.Group.Synonym

URI: https://scilib.ai/kg/mathlib#instMonoidColex

English

If α is a Monoid, then Colex α naturally carries a Monoid structure.

Русский

Если α — моноид, то Colex α естественным образом имеет моноидальную структуру.

LaTeX

$$$Monoid(\alpha) \Rightarrow Monoid(\mathrm{Colex} \alpha)$$$

Lean4

@[to_additive]
instance [h : Monoid α] : Monoid (Colex α) :=
  h

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

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

Разделы

Аффилиация

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