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 m and n greater than 1 is m * n - m - n. This result is also known as the Chicken McNugget Theorem.

Implementation Notes #

First we define Frobenius numbers in general using is_greatest and add_submonoid.closure. Then we proceed to compute the Frobenius number of m and n.

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 and 0 mod m, then show it is at most k. Then k_1 is a multiple of m, so (k-k_1) is a multiple of n, and we're done.

Tags #

frobenius number, chicken mcnugget, chinese remainder theorem, add_submonoid.closure

source

def is_frobenius_number (n : ℕ) (s : set ℕ) :

Prop

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 s. In other words, it is the largest number that can not be expressed as a sum of numbers in s.

Equations

is_frobenius_number n s = is_greatest {k : ℕ | k ∉ add_submonoid.closure s} n

source

theorem is_frobenius_number_pair {m n : ℕ} (cop : m.coprime n) (hm : 1 < m) (hn : 1 < n) :

is_frobenius_number (m * n - m - n) {m, n}

The Chicken Mcnugget theorem stating that the Frobenius number of positive numbers m and n is m * n - m - n.