Theorem Finset.isDiag_mk_of_mem_diag

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.isDiag_mk_of_mem_diagView on Github →
2023-11-18 03:56
Mathlib/Data/Finset/Sym.lean
feat: remove `DecidableEq` argument from `Finset.sym2` (#8211)
Added Finset.isDiag_mk_of_mem_diagView on Github →