bot

Mathlib.GroupTheory.Finiteness

URI: https://scilib.ai/kg/mathlib#Submonoid.FG.bot

English

The bottom submonoid is finitely generated (by the empty generating set).

Русский

Нижний подмножество порождено пустым набором и следовательно FG.

LaTeX

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

Lean4

@[to_additive]
theorem bot : FG (⊥ : Submonoid M) :=
  ⟨∅, by simp⟩

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

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

Разделы

Аффилиация

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