to_moduleFinite_int — Mathlib

English

If G is a finitely generated abelian group, then G is finitely generated as a ℤ-module.

Русский

Если G — конечно порождаемая абелева группа, то она конечно порождается как модуль над целыми числами.

LaTeX

$$AddGroup.FG G ⇒ Module.Finite Int G$$

Lean4

instance to_moduleFinite_int {G : Type*} [AddCommGroup G] [FG G] : Module.Finite ℤ G :=
  Module.Finite.iff_addGroup_fg.mpr <| AddGroup.fg_iff_addMonoid_fg.mpr ‹_›

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