Theorem Finpartition.card_parts_le_card

Modification history

2024-06-04 08:34

Mathlib/Order/Partition/Finpartition.lean

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

Modified Finpartition.card_parts_le_card View on Github →

2023-02-04 13:28

Mathlib/Order/Partition/Finpartition.lean

feat: port Order.Partition.Finpartition (#1765)

Added Finpartition.card_parts_le_card View on Github →