fg_bot

Mathlib.RingTheory.Adjoin.FG

URI: https://scilib.ai/kg/mathlib#Subalgebra.fg_bot

English

The bottom subalgebra is finitely generated.

Русский

Нижняя подалгебра конечнопорождена.

LaTeX

$$$ (\\perp : Subalgebra\\ R\\ A).FG $$$

Lean4

theorem fg_bot : (⊥ : Subalgebra R A).FG :=
  ⟨∅, Finset.coe_empty ▸ Algebra.adjoin_empty R A⟩

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

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

Разделы

Аффилиация

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