Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-29 05:57 6c046c75

View on Github →

chore(data/setoid): split into basic and partition (#2853) The basic part has slightly fewer dependencies and partition part is never used in mathlib.

Estimated changes

deleted def setoid.classes
deleted theorem setoid.classes_inj
deleted theorem setoid.classes_mk_classes
modified def setoid.correspondence
deleted theorem setoid.eq_iff_classes_eq
deleted theorem setoid.eq_of_mem_classes
deleted theorem setoid.eqv_class_mem
deleted def setoid.is_partition
added theorem setoid.ker_def
deleted theorem setoid.mem_classes
deleted def setoid.mk_classes
deleted theorem setoid.mk_classes_classes
added def setoid.classes
added theorem setoid.classes_inj
added theorem setoid.eqv_class_mem
added theorem setoid.mem_classes