Chicken Mcnugget/Frobenius coin

Stream: Is there code for X?

[Alex Zhao]

Chicken Mcnugget theorem: smallest number you can "build" from nonnegative multiples of m, n in naturals is m*n-m-n. Is this in Mathlib yet?

[Johan Commelin]

Nope, I don't think so.

[Kevin Buzzard]

I think that's the largest number you can't build :-) and it should be a nice exercise in Lean.

[Damiano Testa]

Also, I encourage you to assume that m and n are relatively prime!

[Alex Zhao]

sorry yes, largest number you cant build assume coprimality my bad

[Aaron Anderson]

I’ve been advising @Alex Zhao on this, and now he has a nearly-PR-able version. Do we have any thoughts as to where this could belong in mathlib, perhaps in archive?

[Scott Morrison]

I think it should just go in mathlib proper.

[Scott Morrison]

Presumably in the form of an implication x > m * n - m - n implies \exists ....

[Mario Carneiro]

that's the easy direction, isn't it?

[Scott Morrison]

oh yes :-)

[Scott Morrison]

and I guess just \forall a b, a * m + b * n \ne m * n - m - n.

[Scott Morrison]

(The point I was attempting to make is that one shouldn't state this theorem as the sup of a set.)

[Scott Morrison]

and it could just go in mathlib as early as the import structure allows.