Frobenius Number in Two Variables #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we first define a predicate for Frobenius numbers, then solve the 2-variable variant of this problem.
Theorem Statement #
Given a finite set of relatively prime integers all greater than 1, their Frobenius number is the
largest positive integer that cannot be expressed as a sum of nonnegative multiples of these
integers. Here we show the Frobenius number of two relatively prime integers
than 1 is
m * n - m - n. This result is also known as the Chicken McNugget Theorem.
Implementation Notes #
For the upper bound, we begin with an auxiliary lemma showing
m * n is not attainable, then show
m * n - m - n is not attainable. Then for the construction, we create a
k_1 which is
k mod n
0 mod m, then show it is at most
k_1 is a multiple of
is a multiple of n, and we're done.
frobenius number, chicken mcnugget, chinese remainder theorem, add_submonoid.closure
A natural number
n is the Frobenius number of a set of natural numbers
s if it is an
upper bound on the complement of the additive submonoid generated by
In other words, it is the largest number that can not be expressed as a sum of numbers in