fg_of_monoid_fg

Mathlib.GroupTheory.Finiteness

URI: https://scilib.ai/kg/mathlib#AddMonoid.fg_of_monoid_fg

English

If a monoid M is finitely generated, then its additive version Additive M is finitely generated.

Русский

Если моноид M конечнопорожден, то Additive M также конечнопорожден.

LaTeX

$$$\\text{[Monoid.FG M]} \\Rightarrow \\text{AddMonoid.FG (Additive M)}$$$

Lean4

instance fg_of_monoid_fg [Monoid.FG M] : AddMonoid.FG (Additive M) :=
  Monoid.fg_iff_add_fg.1 ‹_›

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

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

Разделы

Аффилиация

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