Commit 2025-09-12 22:44 2d33bff4

View on Github →

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

Estimated changes

Modified Mathlib/Data/Set/Finite/Basic.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

modified theorem dvd_generator_iff

Modified Mathlib/NumberTheory/FrobeniusNumber.lean

added theorem Nat.addSubmonoid_fg

added theorem Nat.dvdNotUnit_setGcd_insert

added theorem Nat.dvd_setGcd_iff

added theorem Nat.exists_mem_closure_of_ge

added theorem Nat.exists_mem_span_nat_finset_of_ge

added theorem Nat.exists_ne_zero_of_setGcd_ne_zero

added theorem Nat.finite_setOf_setGcd_dvd_and_mem_span

added theorem Nat.setGcd_dvd_of_mem

added theorem Nat.setGcd_dvd_of_mem_closure

added theorem Nat.setGcd_eq_zero_iff

added theorem Nat.setGcd_insert_of_dvd

added theorem Nat.setGcd_mono

added theorem Nat.span_singleton_setGcd

added theorem Nat.subset_span_setGcd

added theorem exists_frobeniusNumber_iff

added theorem frobeniusNumber_iff

Modified Mathlib/RingTheory/Ideal/NatInt.lean

modified theorem Nat.maximalIdeal_eq_span_two_three

added theorem Nat.one_mem_closure_iff

added theorem Nat.one_mem_span_iff

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

added theorem Submodule.IsPrincipal.dvd_generator_span_iff