mathlib
f2fdef6f - feat(order/partition/equipartition): Equipartitions (#12023)

Commit
3 years ago
feat(order/partition/equipartition): Equipartitions (#12023) Define `finpartition.is_equipartition`, a predicate for saying that the parts of a `finpartition` of a `finset` are all the same size up to a difference of `1`. Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com>
Author
Parents
Loading