Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finpartition.is_equipartition.card_parts_eq_average

Modification history

2022-03-31 02:41

src/order/partition/equipartition.lean

feat(combinatorics/simple_graph/regularity/bound): Numerical bounds for Szemerédi's regularity lemma (#12962) …

Added finpartition.is_equipartition.card_parts_eq_average View on Github →