fg_of_finiteType — Mathlib

English

If the monoid algebra R[M] is finitely generated as an R-algebra, then M is finitely generated as a monoid.

Русский

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

LaTeX

$$$\text{FiniteType}_R(\mathrm{MonoidAlgebra}\,R\,M) \Rightarrow \mathrm{Monoid.FG}\,M$$$

Lean4

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

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