English
Every additive submonoid of the natural numbers is finitely generated.
Русский
Каждое добавочное подмоноид натуральных чисел порождается конечным количеством элементов.
LaTeX
$$$\\forall s:\\mathrm{AddSubmonoid}\\,\\mathbb{N},\\; s.FG$$$
Lean4
/-- `ℕ` is a Noetherian `ℕ`-module, i.e., `ℕ` is a Noetherian semiring. -/
instance : IsNoetherian ℕ ℕ where
noetherian
s := by
have ⟨t, n, hts, hn⟩ := exists_mem_span_nat_finset_of_ge s
classical
refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩
· simpa using ⟨hts, fun _ ↦ And.right⟩
obtain le | gt := le_or_gt n m
· exact Submodule.span_mono (by simp) (hn m le (setGcd_dvd_of_mem hm))
· exact Submodule.subset_span (by simpa using .inr ⟨gt, hm⟩)
