Documentation

Mathlib.Order.Partition.Equipartition

Finite equipartitions #

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

Main declarations #

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

Instances For

    Discrete and indiscrete finpartition #