Theorem Setoid.eq_of_mem_eqv_class

Modification history

2024-04-24 14:51
Mathlib/Data/Setoid/Partition.lean
feat: `∃! x ∈ s, p x` syntax (#12237) …
Modified Setoid.eq_of_mem_eqv_classView on Github →
2024-04-18 05:39
Mathlib/Data/Setoid/Partition.lean
feat: make `ExistsUnique` notation throw an error when used with more than one binder (#12218) …
Modified Setoid.eq_of_mem_eqv_classView on Github →
2023-06-12 01:02
Mathlib/Data/Setoid/Partition.lean
chore: formatting issues (#4947)
Modified Setoid.eq_of_mem_eqv_classView on Github →
2023-02-06 01:05
Mathlib/Data/Setoid/Partition.lean
feat: port Data.Setoid.Partition (#2066) …
Added Setoid.eq_of_mem_eqv_classView on Github →