LeanAide GPT-4 documentation

Module: Mathlib.NumberTheory.FrobeniusNumber


frobeniusNumber_pair

theorem frobeniusNumber_pair : ∀ {m n : ℕ}, m.Coprime n → 1 < m → 1 < n → FrobeniusNumber (m * n - m - n) {m, n} := by sorry

The **Chicken McNugget Theorem** states that for any two coprime natural numbers `m` and `n`, both greater than one, the Frobenius number (the largest number that cannot be expressed as a sum of any combination of `m` and `n`) is calculated by the formula `m * n - m - n`.

More concisely: For coprime natural numbers `m` and `n` greater than one, the Frobenius number is `m * n - m - n`.