fg_def

Mathlib.GroupTheory.Finiteness

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

English

For any monoid M, Monoid.FG M holds iff the top submonoid is FG, i.e., FG is equivalent to FG on ⊤.

Русский

Для любого моноида M справедливо: Monoid.FG M эквивалентно FG верхнего подмонойда ⊤.

LaTeX

$$$\\text{Monoid.FG } M \\iff (\\top : \\text{Submonoid } M).FG$$$

Lean4

@[to_additive]
theorem fg_def : Monoid.FG M ↔ (⊤ : Submonoid M).FG :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

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

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

Разделы

Аффилиация

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