iff_addGroup_fg — Mathlib

English

An additive group G is finitely generated as a ℤ-module if and only if it is finitely generated as an additive group.

Русский

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

LaTeX

$$$\text{Module.Finite } \mathbb{Z} G \iff \text{AddGroup.FG } G$$$

Lean4

theorem iff_addGroup_fg {G : Type*} [AddCommGroup G] : Module.Finite ℤ G ↔ AddGroup.FG G :=
  ⟨fun h => AddGroup.fg_def.2 <| (Submodule.fg_iff_addSubgroup_fg ⊤).1 (finite_def.1 h), fun h =>
    finite_def.2 <| (Submodule.fg_iff_addSubgroup_fg ⊤).2 (AddGroup.fg_def.1 h)⟩

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