Commit 2023-11-18 03:56 b9e2e656

View on Github →

feat: remove DecidableEq argument from Finset.sym2 (#8211)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finset/Sym.lean

added theorem Finset.card_sym2

added theorem Finset.injective_sym2

deleted theorem Finset.isDiag_mk'_of_mem_diag

added theorem Finset.isDiag_mk_of_mem_diag

modified theorem Finset.mem_sym2_iff

deleted theorem Finset.mk'_mem_sym2_iff

added theorem Finset.mk_mem_sym2_iff

added theorem Finset.monotone_sym2

deleted theorem Finset.not_isDiag_mk'_of_mem_offDiag

added theorem Finset.not_isDiag_mk_of_mem_offDiag

added theorem Finset.strictMono_sym2

added theorem Finset.sym2_eq_image

modified theorem Finset.sym2_mono

modified theorem Finset.sym2_singleton

added theorem Finset.sym2_toFinset

modified theorem Finset.sym2_univ

Created Mathlib/Data/List/Sym.lean

added theorem List.first_mem_of_cons_mem_sym

added theorem List.left_mem_of_mk_mem_sym2

added theorem List.length_sym2

added theorem List.length_sym

added theorem List.mem_of_mem_of_mem_sym

added theorem List.mem_sym2_cons_iff

added theorem List.mem_sym2_iff

added theorem List.mk_mem_sym2

added theorem List.mk_mem_sym2_iff

added theorem List.right_mem_of_mk_mem_sym2

added theorem List.sym2_eq_nil_iff

added theorem List.sym2_eq_sym_two

added theorem List.sym_map

added theorem List.sym_one_eq

added theorem List.sym_sublist_sym_cons

Created Mathlib/Data/Multiset/Sym.lean

added theorem Multiset.card_sym2

added theorem Multiset.mem_sym2_iff

added theorem Multiset.mk_mem_sym2_iff

added theorem Multiset.monotone_sym2

added theorem Multiset.sym2_coe

added theorem Multiset.sym2_eq_zero_iff

added theorem Multiset.sym2_mono

Modified Mathlib/Data/Sym/Basic.lean

added theorem Sym.exists_cons_of_mem

added theorem Sym.not_mem_nil

Modified Mathlib/Data/Sym/Card.lean

deleted theorem Finset.card_sym2

modified theorem Sym2.card_image_diag