Discrete Fair Division

Stream: mathlib4

[Shreyas Srinivas]

Given recent PRs to add auction theory and game theory, I wanted to ask if the definitions of discrete fair division theory will be of interest to add into mathlib. This is an area that is mostly combinatorics.

[Shreyas Srinivas]

I have had some of the basic definitions and API lemmas for a few months now

[Shreyas Srinivas]

@Kim Morrison : since you gave the thumbs up, I am assuming you approve. Here is the WIP PR #16253