Commit 2024-04-03 08:17 3b14f80d

View on Github →

feat: Link finpartitions and setoids (#8735)

Estimated changes

Modified Mathlib/Order/Partition/Finpartition.lean

added theorem Finpartition.existsUnique_mem

modified theorem Finpartition.exists_mem

added theorem Finpartition.exists_subset_part_bijOn

added def Finpartition.map

added theorem Finpartition.mem_part

added theorem Finpartition.mem_part_ofSetoid_iff_rel

added def Finpartition.ofSetoid

added def Finpartition.part

added theorem Finpartition.part_mem

added theorem Finpartition.part_surjOn

added theorem Finpartition.parts_map