Theorem Finpartition.not_empty_mem_parts

Modification history

2025-05-25 12:30
Mathlib/Order/Partition/Finpartition.lean
chore(*): not_mem/nmem -> notMem (#25159)
Deleted Finpartition.not_empty_mem_partsView on Github →
2025-03-08 18:10
Mathlib/Order/Partition/Finpartition.lean
chore(Finpartition): review API, golf (#21551)
Added Finpartition.not_empty_mem_partsView on Github →