Theorem Finset.sym2_eq_image

Modification history

2026-02-16 15:42
Mathlib/Data/Finset/Sym.lean
refactor(Data/Sym/Sym2): curry `mk` (#34803) …
Modified Finset.sym2_eq_imageView on Github →
2026-01-13 17:24
Mathlib/Data/Finset/Sym.lean
feat: define `List.offDiag` (#33812) …
Modified Finset.sym2_eq_imageView on Github →
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.sym2_eq_imageView on Github →
2023-11-18 03:56
Mathlib/Data/Finset/Sym.lean
feat: remove `DecidableEq` argument from `Finset.sym2` (#8211)
Added Finset.sym2_eq_imageView on Github →