Theorem Finset.mk_mem_sym2_iff

Modification history

2023-12-27 05:26
Mathlib/Data/Finset/Sym.lean
refactor: remove `Sym2`'s global `Prod` setoid instance, use `s(x, y)` notation for unordered pairs (#8729) …
Modified Finset.mk_mem_sym2_iffView on Github →
2023-11-18 03:56
Mathlib/Data/Finset/Sym.lean
feat: remove `DecidableEq` argument from `Finset.sym2` (#8211)
Added Finset.mk_mem_sym2_iffView on Github →