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