mathlib

6550cbac - feat(order/partition/finpartition): Finite partitions (#9795)

feat(order/partition/finpartition): Finite partitions (#9795) This defines finite partitions along with quite a few constructions, Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>