Commit 2023-02-05 12:45 81507dea

View on Github →

feat: port Order.Partition.Equipartition (#2058)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Partition/Equipartition.lean

added theorem Finpartition.IsEquipartition.average_le_card_part

added theorem Finpartition.IsEquipartition.card_part_le_average_add_one

added theorem Finpartition.IsEquipartition.card_parts_eq_average

added def Finpartition.IsEquipartition

added theorem Finpartition.Set.Subsingleton.isEquipartition

added theorem Finpartition.bot_isEquipartition

added theorem Finpartition.indiscrete_isEquipartition

added theorem Finpartition.isEquipartition_iff_card_parts_eq_average

added theorem Finpartition.top_isEquipartition