fg_iff_mul_fg

Mathlib.GroupTheory.Finiteness

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.fg_iff_mul_fg

← MathLib Explorer

English

The smallest submonoid, namely the bottom element ⊥, is finitely generated.

Русский

Наименьшее подмножество, то есть ⊥, является конечнопорожденным.

LaTeX

$$$ FG(\\bot) $$$

Lean4

theorem fg_iff_mul_fg {M : Type*} [AddMonoid M] (P : AddSubmonoid M) : P.FG ↔ P.toSubmonoid.FG := by
  convert (Submonoid.fg_iff_add_fg (toSubmonoid P)).symm

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

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

Разделы

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

Аффилиация

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