mathlib3 documentation

order.partition.equipartition

Finite equipartitions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
Prop

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

Equations

Discrete and indiscrete finpartition #