Mathlib Changelog
v4
Changelog
About
Github
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