Theorems · Theorem · number theory

exists_frobeniusNumber_iff

∀ {s : Set ℕ}, (∃ n, FrobeniusNumber n s) ↔ Nat.setGcd s = 1 ∧ 1 ∉ s

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.

Defined in

Mathlib.NumberTheory.FrobeniusNumber

Cited by

0 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound