addSubmonoid_fg — Mathlib

English

Every additive submonoid of the natural numbers is finitely generated.

Русский

Каждое добавочное подмоноид натуральных чисел порождается конечным количеством элементов.

LaTeX

$$$\\forall s:\\mathrm{AddSubmonoid}\\,\\mathbb{N},\\; s.FG$$$

Lean4

theorem addSubmonoid_fg (s : AddSubmonoid ℕ) : s.FG :=
  by
  rw [← s.toNatSubmodule_toAddSubmonoid, ← Submodule.fg_iff_addSubmonoid_fg]
  apply IsNoetherian.noetherian

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