fg_adjoin_finset

Mathlib.RingTheory.Adjoin.FG

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

English

For a finite set s, the subalgebra generated by s is finitely generated.

Русский

Для конечного множества s подалгебра, порождаемая s, конечнопорождена.

LaTeX

$$$\\text{FG}(\\operatorname{adjoin}_R(\\uparrow s))$$$

Lean4

theorem fg_adjoin_finset (s : Finset A) : (Algebra.adjoin R (↑s : Set A)).FG :=
  ⟨s, rfl⟩

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

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

Разделы

Аффилиация

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