Commit 2024-06-04 08:34 582ddf8c

View on Github →

feat: part-preserving equivalence of an equipartition with Fin s.card (#12196) Part of #9317.

Estimated changes

Modified Mathlib/Order/Partition/Equipartition.lean

added theorem Finpartition.IsEquipartition.card_large_parts_eq_mod

added theorem Finpartition.IsEquipartition.card_part_eq_average_iff

added theorem Finpartition.IsEquipartition.card_small_parts_eq_mod

added theorem Finpartition.IsEquipartition.exists_partPreservingEquiv

added theorem Finpartition.IsEquipartition.exists_partsEquiv

added theorem Finpartition.IsEquipartition.filter_ne_average_add_one_eq_average

Modified Mathlib/Order/Partition/Finpartition.lean

added theorem Finpartition.card_mod_card_parts_le

modified theorem Finpartition.card_parts_le_card

added def Finpartition.equivSigmaParts

added theorem Finpartition.exists_enumeration