iff_addMonoid_fg — Mathlib

English

If M is finitely generated as an additive monoid, then M is finitely generated as a module over ℕ.

Русский

Если M конечно порождается как аддитивный моноид, то M конечно порождается как модуль над ℕ.

LaTeX

$$$(\text{AddMonoid.FG } M) \Rightarrow \text{Module.Finite } \mathbb{N} M$$$

Lean4

theorem iff_addMonoid_fg {M : Type*} [AddCommMonoid M] : Module.Finite ℕ M ↔ AddMonoid.FG M :=
  ⟨fun h => AddMonoid.fg_def.2 <| (Submodule.fg_iff_addSubmonoid_fg ⊤).1 (finite_def.1 h), fun h =>
    finite_def.2 <| (Submodule.fg_iff_addSubmonoid_fg ⊤).2 (AddMonoid.fg_def.1 h)⟩

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