Documentation

Mathlib.NumberTheory.FrobeniusNumber

Frobenius Number in Two Variables #

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 IsGreatest and AddSubmonoid.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

def FrobeniusNumber (n : ) (s : Set ) :

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
Instances For
    theorem frobeniusNumber_pair {m : } {n : } (cop : Nat.Coprime m n) (hm : 1 < m) (hn : 1 < n) :
    FrobeniusNumber (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.