exists_frobeniusNumber_iff — Mathlib

English

There exists a Frobenius number for a set s if and only if gcd(s) = 1 and 1 ∉ s.

Русский

Существует число Фробениуса для множества s тогда и только тогда, когда gcd(s) = 1 и 1 ∉ s.

LaTeX

$$$\\exists n\\, \\mathrm{FrobeniusNumber}(n,s) \\iff \\mathrm{setGcd}(s) = 1 \\land 1 \\notin s$$$

Lean4

/-- 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)

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