mathlib

d3f5adb0 - feat(combinatorics/simple_graph/regularity/equitabilise): Equitabilising a partition (#13222)

feat(combinatorics/simple_graph/regularity/equitabilise): Equitabilising a partition (#13222) Define the equitabilisation of a partition and a way to find an arbitrary equipartition of any size. Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com>