Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-23 23:02 584ae9db

View on Github →

chore(data/{lists,multiset}/*): More dot notation (#12876) Rename many list and multiset lemmas to make them eligible to dot notation. Also add a few aliases to lemmas for even more dot notation. Renames

Estimated changes

modified def finset.erase
modified def finset.filter
modified theorem finset.image_val_of_inj_on
modified theorem finset.insert_def
modified def
modified theorem finset.not_mem_erase
deleted theorem list.mem_erase_of_nodup
added theorem list.nodup.append
added theorem list.nodup.diff
added theorem list.nodup.erase
added theorem list.nodup.filter
added theorem list.nodup.insert
added theorem list.nodup.inter
added theorem list.nodup.map_on
added theorem list.nodup.not_mem
added theorem list.nodup.of_cons
added theorem list.nodup.of_map
added theorem list.nodup.pmap
added theorem list.nodup.sigma
added theorem list.nodup.union
deleted theorem list.nodup_concat
deleted theorem list.nodup_cons_of_nodup
deleted theorem list.nodup_diff
deleted theorem list.nodup_erase_of_nodup
deleted theorem list.nodup_filter
deleted theorem list.nodup_filter_map
deleted theorem list.nodup_insert
deleted theorem list.nodup_inter_of_nodup
deleted theorem list.nodup_map
deleted theorem list.nodup_map_on
deleted theorem list.nodup_of_nodup_cons
deleted theorem list.nodup_of_nodup_map
deleted theorem list.nodup_of_sublist
deleted theorem list.nodup_pmap
deleted theorem list.nodup_product
deleted theorem list.nodup_sigma
modified theorem list.nodup_singleton
modified theorem list.nodup_sublists_len
deleted theorem list.nodup_union
deleted theorem list.nodup_update_nth
modified theorem list.not_nodup_cons_of_mem
added theorem multiset.nodup.add_iff
added theorem multiset.nodup.cons
added theorem multiset.nodup.erase
added theorem multiset.nodup.ext
added theorem multiset.nodup.filter
added theorem
added theorem multiset.nodup.map_on
added theorem multiset.nodup.not_mem
added theorem multiset.nodup.of_cons
added theorem multiset.nodup.of_map
added theorem multiset.nodup.pmap
deleted theorem multiset.nodup_ext
deleted theorem multiset.nodup_filter
deleted theorem multiset.nodup_filter_map
deleted theorem multiset.nodup_inter_left
deleted theorem multiset.nodup_map
deleted theorem multiset.nodup_map_on
deleted theorem multiset.nodup_pmap
deleted theorem multiset.nodup_product
deleted theorem multiset.nodup_sigma