Commit 2025-03-08 18:10 c30d062e

View on Github →

chore(Finpartition): review API, golf (#21551)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Turan.lean

Modified Mathlib/Order/Partition/Finpartition.lean

deleted theorem Finpartition.mem_part

added theorem Finpartition.mem_part_iff_exists

added theorem Finpartition.mem_part_self

added theorem Finpartition.ne_empty

added theorem Finpartition.not_empty_mem_parts

added theorem Finpartition.part_eq_empty

added theorem Finpartition.part_eq_iff_mem

modified theorem Finpartition.part_eq_of_mem

modified theorem Finpartition.part_mem

added theorem Finpartition.part_nonempty

added theorem Finpartition.part_subset