fg_of_finiteType

Mathlib.RingTheory.FiniteType

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.fg_of_finiteType

← MathLib Explorer

English

If the monoid algebra R[M] is of finite type, then M is finitely generated.

Русский

Если R[M] конечного типа, то M порожден конечным набором.

LaTeX

$$$\\mathrm{FiniteType}(R,R[M]) \\Rightarrow \\mathrm{FG}(M)$$$

Lean4

/-- If `R[M]` is of finite type then `M` is finitely generated. -/
theorem fg_of_finiteType [CommRing R] [Nontrivial R] [h : FiniteType R R[M]] : AddMonoid.FG M :=
  finiteType_iff_fg.1 h

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

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

Разделы

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

Аффилиация

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