finiteType_iff_group_fg — Mathlib

English

A group G is finitely generated if and only if the monoid algebra R[G] is finitely generated as an R-algebra.

Русский

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

LaTeX

$$$\mathrm{FiniteType}\,R(\mathrm{MonoidAlgebra}\,R\,G) \iff \mathrm{Group.FG}\,G$$$

Lean4

/-- A group `G` is finitely generated if and only if `R[G]` is of finite type. -/
theorem finiteType_iff_group_fg {G : Type*} [Group G] [CommRing R] [Nontrivial R] :
    FiniteType R (MonoidAlgebra R G) ↔ Group.FG G := by simpa [Group.fg_iff_monoid_fg] using finiteType_iff_fg

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