Commit 2023-01-13 14:55 7df37a9a

View on Github →

feat: port Data.Multiset.Dedup (#1541)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/Dedup.lean

added theorem Multiset.Nodup.le_dedup_iff_le

added theorem Multiset.Nodup.le_nsmul_iff_le

added theorem Multiset.coe_dedup

added theorem Multiset.count_dedup

added def Multiset.dedup

added theorem Multiset.dedup_bind_dedup

added theorem Multiset.dedup_cons_of_mem

added theorem Multiset.dedup_cons_of_not_mem

added theorem Multiset.dedup_eq_self

added theorem Multiset.dedup_eq_zero

added theorem Multiset.dedup_ext

added theorem Multiset.dedup_idempotent

added theorem Multiset.dedup_le

added theorem Multiset.dedup_map_dedup_eq

added theorem Multiset.dedup_nsmul

added theorem Multiset.dedup_singleton

added theorem Multiset.dedup_subset'

added theorem Multiset.dedup_subset

added theorem Multiset.dedup_zero

added theorem Multiset.le_dedup

added theorem Multiset.le_dedup_self

added theorem Multiset.mem_dedup

added theorem Multiset.nodup_dedup

added theorem Multiset.subset_dedup'

added theorem Multiset.subset_dedup