fg_of_group_fg

Mathlib.GroupTheory.Finiteness

URI: https://scilib.ai/kg/mathlib#Monoid.fg_of_group_fg

English

If a group G is finitely generated, then G is finitely generated as a monoid.

Русский

Если группа G конечно порождена как группа, то она конечно порождена как моноид.

LaTeX

$$$\text{Group.FG}(G) \Rightarrow \text{Monoid.FG}(G)$$$

Lean4

@[to_additive]
instance fg_of_group_fg [Group.FG G] : Monoid.FG G :=
  Group.fg_iff_monoid_fg.1 ‹_›

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

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

Разделы

Аффилиация

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