Theorem Setoid.eq_eqv_class_of_mem
Modification history
2024-04-24 14:51
Mathlib/Data/Setoid/Partition.lean
feat: `∃! x ∈ s, p x` syntax (#12237) …
Modified Setoid.eq_eqv_class_of_memView 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_eqv_class_of_memView on Github →