mathlib documentation


Finite equipartitions #

This file defines finite equipartitions, the partitions whose parts all are the same size up to a difference of 1.

Main declarations #

def finpartition.is_equipartition {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) :

An equipartition is a partition whose parts are all the same size, up to a difference of 1.


Discrete and indiscrete finpartition #