Commit 2020-10-01 02:57 1b973263

feat(data/fintype): pigeonhole principles (#4096) Add pigeonhole principles for finitely and infinitely many pigeons in finitely many holes. There are also strong versions of these, which say that there is a hole containing at least as many pigeons as the average number of pigeons per hole. Fixes #2272.