finiteType_iff_group_fg — Mathlib

English

A additive group G is finitely generated iff its group algebra R[G] is finite type.

Русский

Дополнительная группа G конечна порождена тогда и только тогда, когда R[G] конечного типа.

LaTeX

$$$\\mathrm{FiniteType}(R,R[G]) \\iff \\mathrm{FG}(G)$$$

Lean4

/-- An additive group `G` is finitely generated if and only if `R[G]` is of
finite type. -/
theorem finiteType_iff_group_fg {G : Type*} [AddGroup G] [CommRing R] [Nontrivial R] :
    FiniteType R R[G] ↔ AddGroup.FG G := by simpa [AddGroup.fg_iff_addMonoid_fg] using finiteType_iff_fg

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