feat(NumberTheory): Frobenius number exists & ℕ is Noetherian semiring (#27743)

+ The Frobenius number of a set of natural numbers exist iff the set has gcd 1 and doesn't contain 1.

+ All additive submonoids (= ideals) of ℕ are finitely generated.

+ The game of Sylver coinage always terminates.

This is the outcome of a course project at Heidelberg University: [matematiflo.github.io/CompAssistedMath2025](https://matematiflo.github.io/CompAssistedMath2025/)

Co-authored-by: Daniel Buth @greymatter8
Co-authored-by: Sebastian Meier @SebastianMeierUni

Author: alreadydone

Mathlib/Data/Set/Finite/Basic.lean

@@ -388,6 +388,17 @@ end Multiset
 theorem List.finite_toSet (l : List α) : { x | x ∈ l }.Finite :=
   (show Multiset α from ⟦l⟧).finite_toSet
 
+/-- `Finset α` is order isomorphic to the type of finite sets in `α`. -/
+@[simps] noncomputable def OrderIso.finsetSetFinite : Finset α ≃o {s : Set α // s.Finite} where
+  toFun s := ⟨s, s.finite_toSet⟩
+  invFun s := s.2.toFinset
+  left_inv _ := by simp
+  right_inv _ := by simp
+  map_rel_iff' := .rfl
+
+instance : WellFoundedLT {s : Set α // s.Finite} :=
+  OrderIso.finsetSetFinite.symm.toOrderEmbedding.wellFoundedLT
+
 /-! ### Finite instances
 
 There is seemingly some overlap between the following instances and the `Fintype` instances

Mathlib/LinearAlgebra/FreeModule/PID.lean

@@ -81,21 +81,11 @@ theorem eq_bot_of_generator_maximal_submoduleImage_eq_zero {N O : Submodule R M}
 
 end Ring
 
-section IsDomain
-
-variable {ι : Type*} {R : Type*} [CommRing R] [IsDomain R]
-variable {M : Type*} [AddCommGroup M] [Module R M] {b : ι → M}
-
-open Submodule.IsPrincipal Set Submodule
-
-theorem dvd_generator_iff {I : Ideal R} [I.IsPrincipal] {x : R} (hx : x ∈ I) :
-    x ∣ generator I ↔ I = Ideal.span {x} := by
-  conv_rhs => rw [← span_singleton_generator I]
-  rw [Ideal.submodule_span_eq, Ideal.span_singleton_eq_span_singleton, ← dvd_dvd_iff_associated,
-    ← mem_iff_generator_dvd]
-  exact ⟨fun h ↦ ⟨hx, h⟩, fun h ↦ h.2⟩
-
-end IsDomain
+open Submodule.IsPrincipal in
+theorem dvd_generator_iff {R : Type*} [CommSemiring R] {I : Ideal R} [I.IsPrincipal] {x : R}
+    (hx : x ∈ I) : x ∣ generator I ↔ I = Ideal.span {x} := by
+  simp_rw [le_antisymm_iff, I.span_singleton_le_iff_mem.2 hx, and_true, ← Ideal.mem_span_singleton]
+  conv_rhs => rw [← span_singleton_generator I, Submodule.span_singleton_le_iff_mem]
 
 section PrincipalIdealDomain
 
@@ -106,7 +96,7 @@ variable {M : Type*} [AddCommGroup M] [Module R M] {b : ι → M}
 
 section StrongRankCondition
 
-variable [IsDomain R] [IsPrincipalIdealRing R]
+variable [IsPrincipalIdealRing R]
 
 open Submodule.IsPrincipal
 
@@ -142,6 +132,8 @@ theorem generator_maximal_submoduleImage_dvd {N O : Submodule R M} (hNO : N ≤
     exact Ideal.span_singleton_le_span_singleton.mpr d_dvd_left
   · exact subset_span (mem_insert _ _)
 
+variable [IsDomain R]
+
 /-- The induction hypothesis of `Submodule.basisOfPid` and `Submodule.smithNormalForm`.
 
 Basically, it says: let `N ≤ M` be a pair of submodules, then we can find a pair of

Mathlib/NumberTheory/FrobeniusNumber.lean

@@ -1,18 +1,17 @@
 /-
 Copyright (c) 2021 Alex Zhao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Alex Zhao
+Authors: Alex Zhao, Daniel Buth, Sebastian Meier, Junyan Xu
 -/
-import Mathlib.Algebra.Group.Submonoid.Membership
-import Mathlib.Data.Nat.ModEq
-import Mathlib.Tactic.Ring
-import Mathlib.Tactic.Zify
+import Mathlib.RingTheory.Ideal.NatInt
 
 /-!
-# Frobenius Number in Two Variables
+# Frobenius Number
 
 In this file we first define a predicate for Frobenius numbers, then solve the 2-variable variant
-of this problem.
+of this problem. We also show the Frobenius number exists for any set of coprime natural numbers
+that doesn't contain 1. This is closely related to the fact that all ideals of ℕ are finitely
+generated, which we also prove in this file.
 
 ## Theorem Statement
 
@@ -33,7 +32,7 @@ is a multiple of n, and we're done.
 
 ## Tags
 
-frobenius number, chicken mcnugget, chinese remainder theorem, add_submonoid.closure
+frobenius number, chicken mcnugget, chinese remainder theorem, AddSubmonoid.closure
 -/
 
 
@@ -45,6 +44,10 @@ In other words, it is the largest number that cannot be expressed as a sum of nu
 def FrobeniusNumber (n : ℕ) (s : Set ℕ) : Prop :=
   IsGreatest { k | k ∉ AddSubmonoid.closure s } n
 
+theorem frobeniusNumber_iff {n : ℕ} {s : Set ℕ} :
+    FrobeniusNumber n s ↔ n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s := by
+  simp_rw [FrobeniusNumber, IsGreatest, upperBounds, Set.mem_setOf, not_imp_comm, not_le]
+
 variable {m n : ℕ}
 
 /-- The **Chicken McNugget theorem** stating that the Frobenius number
@@ -77,3 +80,147 @@ theorem frobeniusNumber_pair (cop : Coprime m n) (hm : 1 < m) (hn : 1 < n) :
       ModEq.le_of_lt_add
         (x.2.1.trans (modEq_zero_iff_dvd.mpr (Nat.dvd_sub (dvd_mul_right m n) dvd_rfl)).symm)
         (lt_of_lt_of_le hx le_tsub_add)
+
+namespace Nat
+
+open Submodule.IsPrincipal
+
+/-- The gcd of a set of natural numbers is defined to be the nonnegative generator
+of the ideal of `ℤ` generated by them. -/
+noncomputable def setGcd (s : Set ℕ) : ℕ :=
+  (generator <| Ideal.span <| ((↑) : ℕ → ℤ) '' s).natAbs
+
+variable {s t : Set ℕ} {n : ℕ}
+
+lemma setGcd_dvd_of_mem (h : n ∈ s) : setGcd s ∣ n := by
+  rw [setGcd, ← Int.dvd_natCast, ← mem_iff_generator_dvd]
+  exact Ideal.subset_span ⟨n, h, rfl⟩
+
+lemma setGcd_dvd_of_mem_closure (h : n ∈ AddSubmonoid.closure s) : setGcd s ∣ n :=
+  AddSubmonoid.closure_induction (fun _ ↦ setGcd_dvd_of_mem) (dvd_zero _) (fun _ _ _ _ ↦ dvd_add) h
+
+/-- The characterizing property of `Nat.setGcd`. -/
+lemma dvd_setGcd_iff : n ∣ setGcd s ↔ ∀ m ∈ s, n ∣ m := by
+  simp_rw [setGcd, ← Int.natCast_dvd, dvd_generator_span_iff,
+    Set.forall_mem_image, Int.natCast_dvd_natCast]
+
+lemma setGcd_mono (h : s ⊆ t) : setGcd t ∣ setGcd s :=
+  dvd_setGcd_iff.mpr fun _m hm ↦ setGcd_dvd_of_mem (h hm)
+
+lemma dvdNotUnit_setGcd_insert (h : ¬ setGcd s ∣ n) :
+    DvdNotUnit (setGcd (insert n s)) (setGcd s) :=
+  dvdNotUnit_of_dvd_of_not_dvd (setGcd_mono <| Set.subset_insert ..)
+    fun dvd ↦ h <| dvd_setGcd_iff.mp dvd _ (Set.mem_insert ..)
+
+lemma setGcd_insert_of_dvd (h : setGcd s ∣ n) : setGcd (insert n s) = setGcd s :=
+  (setGcd_mono <| Set.subset_insert ..).antisymm <| dvd_setGcd_iff.mpr
+    fun m ↦ by rintro (rfl | hm); exacts [h, setGcd_dvd_of_mem hm]
+
+lemma setGcd_eq_zero_iff : setGcd s = 0 ↔ s ⊆ {0} := by
+  simp_rw [setGcd, Int.natAbs_eq_zero, ← eq_bot_iff_generator_eq_zero, Ideal.span_eq_bot,
+    Set.forall_mem_image, Int.natCast_eq_zero, Set.subset_def, Set.mem_singleton_iff]
+
+lemma exists_ne_zero_of_setGcd_ne_zero (hs : setGcd s ≠ 0) : ∃ n ∈ s, n ≠ 0 := by
+  contrapose! hs
+  exact setGcd_eq_zero_iff.mpr hs
+
+variable (s)
+
+lemma span_singleton_setGcd : Ideal.span {(setGcd s : ℤ)} = Ideal.span (((↑) : ℕ → ℤ) '' s) := by
+  rw [setGcd, ← Ideal.span_singleton_eq_span_singleton.mpr (Int.associated_natAbs _),
+    Ideal.span, span_singleton_generator]
+
+lemma subset_span_setGcd : s ⊆ Ideal.span {setGcd s} :=
+  fun _x hx ↦ Ideal.mem_span_singleton.mpr (setGcd_dvd_of_mem hx)
+
+open Ideal in
+theorem exists_mem_span_nat_finset_of_ge :
+    ∃ (t : Finset ℕ) (n : ℕ), ↑t ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → m ∈ Ideal.span t := by
+  by_cases h0 : setGcd s = 0
+  · refine ⟨∅, 0, by simp, fun _ _ dvd ↦ by cases zero_dvd_iff.mp (h0 ▸ dvd); exact zero_mem _⟩
+  -- Write the gcd of `s` as a ℤ-linear combination of a finite subset `t`.
+  have ⟨t, hts, a, eq⟩ := (Submodule.mem_span_image_iff_exists_fun _).mp
+    (span_singleton_setGcd s ▸ mem_span_singleton_self _)
+  -- Let `x` be an arbitrary nonzero element in `s`.
+  have ⟨x, hxs, hx⟩ := exists_ne_zero_of_setGcd_ne_zero h0
+  let n := (x / setGcd s) * ∑ i, (-a i).toNat * i
+  refine ⟨insert x t, n, by simpa [Set.insert_subset_iff] using ⟨hxs, hts⟩, fun m ge dvd ↦ ?_⟩
+  -- For `m ≥ n`, write `m = q * x + (r + n)` with 0 ≤ r < x.
+  obtain ⟨c, rfl⟩ := exists_add_of_le ge
+  rw [← c.div_add_mod' x]
+  set q := c / x
+  set r := c % x
+  rw [add_comm, add_assoc]
+  refine add_mem (mul_mem_left _ q (subset_span (Finset.mem_insert_self ..)))
+    (Submodule.span_mono (s := t) (Finset.subset_insert ..) ?_)
+  -- It suffices to show `r + n` lies in the ℕ-span of `t`.
+  obtain ⟨rx, hrx⟩ : setGcd s ∣ r := (dvd_mod_iff (setGcd_dvd_of_mem hxs)).mpr <|
+    (Nat.dvd_add_right <| dvd_mul_of_dvd_right (Finset.dvd_sum fun i _ ↦
+      dvd_mul_of_dvd_right (setGcd_dvd_of_mem (hts i.2)) _) _).mp dvd
+  convert (sum_mem fun i _ ↦ mul_mem_left _ _ (subset_span i.2) :
+    -- an explicit ℕ-linear combination of elements of `t` that is equal to `r + n`
+    ∑ i : t, (if 0 ≤ a i then rx else x / setGcd s - rx) * (a i).natAbs * i ∈ span t)
+  simp_rw [← Int.natCast_inj, hrx, n, Finset.mul_sum, mul_comm _ rx, cast_add, cast_sum, cast_mul,
+    ← eq, Finset.mul_sum, smul_eq_mul, ← mul_assoc, ← Finset.sum_add_distrib, ← add_mul]
+  congr! 2 with i
+  split_ifs with hai
+  · rw [Int.toNat_eq_zero.mpr (by omega), cast_zero, mul_zero, add_zero,
+      Int.natCast_natAbs, abs_eq_self.mpr hai]
+  · rw [cast_sub, Int.natCast_natAbs, abs_eq_neg_self.mpr (by omega), sub_mul,
+      ← Int.eq_natCast_toNat.mpr (by omega), mul_neg (rx : ℤ), sub_neg_eq_add, add_comm]
+    rw [← Nat.mul_le_mul_left_iff (pos_of_ne_zero h0), ← hrx,
+      Nat.mul_div_cancel' (setGcd_dvd_of_mem hxs)]
+    exact (c.mod_lt (pos_of_ne_zero hx)).le
+
+theorem exists_mem_closure_of_ge : ∃ n, ∀ m ≥ n, setGcd s ∣ m → m ∈ AddSubmonoid.closure s :=
+  have ⟨_t, n, hts, hn⟩ := exists_mem_span_nat_finset_of_ge s
+  ⟨n, fun m ge dvd ↦ (Submodule.span_nat_eq_addSubmonoidClosure s).le
+    (Submodule.span_mono hts (hn m ge dvd))⟩
+
+theorem finite_setOf_setGcd_dvd_and_mem_span :
+    {n | setGcd s ∣ n ∧ n ∉ Ideal.span s}.Finite :=
+  have ⟨n, hn⟩ := exists_mem_closure_of_ge s
+  (Finset.range n).finite_toSet.subset fun m h ↦ Finset.mem_range.mpr <|
+    lt_of_not_ge fun ge ↦ h.2 <| (Submodule.span_nat_eq_addSubmonoidClosure s).ge (hn m ge h.1)
+
+/-- `ℕ` 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⟩)
+
+theorem addSubmonoid_fg (s : AddSubmonoid ℕ) : s.FG := by
+  rw [← s.toNatSubmodule_toAddSubmonoid, ← Submodule.fg_iff_addSubmonoid_fg]
+  apply IsNoetherian.noetherian
+
+end Nat
+
+/-- A set of natural numbers has a Frobenius number iff their gcd is 1; if 1 is in the set,
+the Frobenius number is -1, so the Frobenius number doesn't exist as a natural number.
+[Wikipedia](https://en.wikipedia.org/wiki/Coin_problem#Statement) seems to attribute this to
+Issai Schur, but [Schur's theorem](https://en.wikipedia.org/wiki/Schur%27s_theorem#Combinatorics)
+is a more precise statement about asymptotics of the number of ℕ-linear combinations, and the
+existence of the Frobenius number for a set with gcd 1 is probably well known before that. -/
+theorem exists_frobeniusNumber_iff {s : Set ℕ} :
+    (∃ n, FrobeniusNumber n s) ↔ setGcd s = 1 ∧ 1 ∉ s where
+  mp := fun ⟨n, hn⟩ ↦ by
+    rw [frobeniusNumber_iff] at hn
+    exact ⟨dvd_one.mp <| Nat.dvd_add_iff_right (setGcd_dvd_of_mem_closure (hn.2 (n + 1)
+      (by omega))) (n := 1) |>.mpr (setGcd_dvd_of_mem_closure (hn.2 (n + 2) (by omega))),
+      fun h ↦ hn.1 <| AddSubmonoid.closure_mono (Set.singleton_subset_iff.mpr h)
+        (addSubmonoidClosure_one.ge ⟨⟩)⟩
+  mpr h := by
+    have ⟨n, hn⟩ := exists_mem_closure_of_ge s
+    let P n := n ∉ AddSubmonoid.closure s
+    have : P 1 := h.2 ∘ one_mem_closure_iff.mp
+    classical
+    refine ⟨findGreatest P n, frobeniusNumber_iff.mpr ⟨findGreatest_spec (P := P) (m := 1)
+      (le_of_not_gt fun lt ↦ this (hn _ lt.le h.1.dvd)) this, fun k gt ↦ ?_⟩⟩
+    obtain le | le := le_total k n
+    · exact of_not_not (findGreatest_is_greatest gt le)
+    · exact hn k le (h.1.dvd.trans <| one_dvd k)

Mathlib/RingTheory/Ideal/NatInt.lean

@@ -34,13 +34,22 @@ theorem Nat.mem_maximalIdeal_iff {n : ℕ} : n ∈ maximalIdeal ℕ ↔ n ≠ 1
 
 theorem Nat.coe_maximalIdeal : (maximalIdeal ℕ : Set ℕ) = {1}ᶜ := by ext; simp
 
-theorem Nat.maximalIdeal_eq_span_two_three : maximalIdeal ℕ = .span {2, 3} := by
+theorem Nat.maximalIdeal_eq_span_two_three : maximalIdeal ℕ = span {2, 3} := by
   refine le_antisymm (fun n h ↦ ?_) (span_le.mpr <| Set.pair_subset (by simp) (by simp))
   obtain lt | lt := (mem_maximalIdeal_iff.mp h).lt_or_gt
   · obtain rfl := lt_one_iff.mp lt; exact zero_mem _
   exact mem_span_pair.mpr <|
     exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le 2 3 n (by simp) (show 2 ≤ n by omega)
 
+theorem Nat.one_mem_span_iff {s : Set ℕ} : 1 ∈ span s ↔ 1 ∈ s := by
+  rw [← SetLike.mem_coe, ← not_iff_not]
+  simp_rw [← Set.mem_compl_iff, ← Set.singleton_subset_iff, Set.subset_compl_comm,
+    ← coe_maximalIdeal, SetLike.coe_subset_coe, span_le]
+
+theorem Nat.one_mem_closure_iff {s : Set ℕ} : 1 ∈ AddSubmonoid.closure s ↔ 1 ∈ s := by
+  rw [← Submodule.span_nat_eq_addSubmonoidClosure]
+  exact one_mem_span_iff
+
 theorem Ideal.isPrime_nat_iff {P : Ideal ℕ} :
     P.IsPrime ↔ P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ p : ℕ, p.Prime ∧ P = span {p} := by
   refine .symm ⟨?_, fun h ↦ or_iff_not_imp_left.mpr fun h0 ↦ or_iff_not_imp_right.mpr fun hsp ↦

Mathlib/RingTheory/PrincipalIdealDomain.lean

@@ -115,9 +115,9 @@ instance (priority := 100) _root_.IsPrincipalIdealRing.of_isNoetherianRing_of_is
 
 end Semiring
 
-section CommRing
+section CommSemiring
 
-variable [CommRing R] [Module R M]
+variable [CommSemiring R] [Module R M]
 
 theorem associated_generator_span_self [IsDomain R] (r : R) :
     Associated (generator <| Ideal.span {r}) r := by
@@ -146,7 +146,14 @@ theorem generator_submoduleImage_dvd_of_mem {N O : Submodule R M} (hNO : N ≤ O
   rw [← mem_iff_generator_dvd, LinearMap.mem_submoduleImage_of_le hNO]
   exact ⟨x, hx, rfl⟩
 
-end CommRing
+theorem dvd_generator_span_iff {r : R} {s : Set R} [(Ideal.span s).IsPrincipal] :
+    r ∣ generator (Ideal.span s) ↔ ∀ x ∈ s, r ∣ x where
+  mp h x hx := h.trans <| (mem_iff_generator_dvd _).mp (Ideal.subset_span hx)
+  mpr h := have : (span R s).IsPrincipal := ‹_›
+    span_induction h (dvd_zero _) (fun _ _ _ _ ↦ dvd_add) (fun _ _ _ ↦ (·.mul_left _))
+      (generator_mem _)
+
+end CommSemiring
 
 end Submodule.IsPrincipal