Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 18:15 8f160018

View on Github →

chore(*): rename erase_dup to dedup (#12057)

Estimated changes

added theorem multiset.gcd_dedup
deleted theorem multiset.gcd_erase_dup
added theorem multiset.lcm_dedup
deleted theorem multiset.lcm_erase_dup
added theorem finset.dedup_eq_self
deleted theorem finset.erase_dup_eq_self
modified theorem finset.image_val
modified theorem finset.insert_val'
modified theorem list.mem_to_finset
modified theorem list.to_finset_val
modified theorem multiset.mem_to_finset
modified def multiset.to_finset
modified theorem multiset.to_finset_val
modified theorem list.card_to_finset
modified theorem multiset.card_to_finset
modified theorem multiset.to_finset_card_le
added theorem list.dedup_append
added theorem list.dedup_cons_of_mem
added theorem list.dedup_eq_self
added theorem list.dedup_idempotent
added theorem list.dedup_nil
added theorem list.dedup_sublist
added theorem list.dedup_subset
added theorem list.mem_dedup
added theorem list.nodup_dedup
added theorem list.subset_dedup
added def list.dedup
deleted def list.erase_dup
deleted theorem list.erase_dup_append
deleted theorem list.erase_dup_eq_self
deleted theorem list.erase_dup_idempotent
deleted theorem list.erase_dup_nil
deleted theorem list.erase_dup_sublist
deleted theorem list.erase_dup_subset
deleted theorem list.mem_erase_dup
deleted theorem list.nodup_erase_dup
deleted theorem list.subset_erase_dup
added theorem list.perm.dedup
deleted theorem list.perm.erase_dup
added def list.dedupkeys
added theorem list.dedupkeys_cons
deleted def list.erase_dupkeys
deleted theorem list.erase_dupkeys_cons
added theorem list.lookup_dedupkeys
deleted theorem list.lookup_erase_dupkeys
added theorem list.sizeof_dedupkeys
deleted theorem list.sizeof_erase_dupkeys
added theorem multiset.coe_dedup
added def multiset.dedup
added theorem multiset.dedup_eq_self
added theorem multiset.dedup_eq_zero
added theorem multiset.dedup_ext
added theorem multiset.dedup_le
added theorem multiset.dedup_nsmul
added theorem multiset.dedup_subset'
added theorem multiset.dedup_subset
added theorem multiset.dedup_zero
added theorem multiset.le_dedup
added theorem multiset.mem_dedup
added theorem multiset.nodup_dedup
added theorem multiset.subset_dedup'
added theorem multiset.subset_dedup
deleted theorem multiset.coe_erase_dup
deleted def multiset.erase_dup
deleted theorem multiset.erase_dup_ext
deleted theorem multiset.erase_dup_le
deleted theorem multiset.erase_dup_nsmul
deleted theorem multiset.erase_dup_subset
deleted theorem multiset.erase_dup_zero
deleted theorem multiset.le_erase_dup
deleted theorem multiset.mem_erase_dup
deleted theorem multiset.nodup_erase_dup
deleted theorem multiset.subset_erase_dup
added theorem multiset.dedup_add
added theorem multiset.dedup_cons
deleted theorem multiset.erase_dup_add
deleted theorem multiset.erase_dup_cons
added theorem multiset.le_smul_dedup
added theorem multiset.inf_dedup
deleted theorem multiset.inf_erase_dup
added theorem multiset.sup_dedup
deleted theorem multiset.sup_erase_dup