fg_of_noetherian

Mathlib.RingTheory.Adjoin.FG

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

← MathLib Explorer

English

If A is Noetherian as an R-algebra, then every subalgebra S is finitely generated.

Русский

Если A — Noetherian по отношению к R-алгебре, то любая подалгебра S FC.

LaTeX

$$$[IsNoetherian\\ R\\ A] \\Rightarrow S.FG$ for any Subalgebra S of A.$$

Lean4

theorem fg_of_noetherian [IsNoetherian R A] (S : Subalgebra R A) : S.FG :=
  fg_of_fg_toSubmodule (IsNoetherian.noetherian (Subalgebra.toSubmodule S))

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

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

Разделы

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

Аффилиация

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