Commit 2023-01-13 14:34 43502ce4

View on Github →

feat: port Data.Multiset.Nodup (#1539)

Estimated changes

Modified Mathlib/Data/Multiset/Nodup.lean

added theorem Multiset.Nodup.add_iff

added theorem Multiset.Nodup.cons

added theorem Multiset.Nodup.erase

added theorem Multiset.Nodup.erase_eq_filter

added theorem Multiset.Nodup.ext

added theorem Multiset.Nodup.filter

added theorem Multiset.Nodup.inter_left

added theorem Multiset.Nodup.inter_right

added theorem Multiset.Nodup.map

added theorem Multiset.Nodup.map_on

added theorem Multiset.Nodup.mem_erase_iff

added theorem Multiset.Nodup.not_mem

added theorem Multiset.Nodup.not_mem_erase

added theorem Multiset.Nodup.of_cons

added theorem Multiset.Nodup.of_map

added theorem Multiset.Nodup.pmap

added theorem Multiset.Pairwise.forall

added theorem Multiset.coe_nodup

added theorem Multiset.count_eq_of_nodup

added theorem Multiset.count_eq_one_of_mem

added theorem Multiset.disjoint_of_nodup_add

added theorem Multiset.inj_on_of_nodup_map

added theorem Multiset.le_iff_subset

added theorem Multiset.map_eq_map_of_bij_of_nodup

added theorem Multiset.mem_sub_of_nodup

added theorem Multiset.nodup_add

added theorem Multiset.nodup_attach

added theorem Multiset.nodup_bind

added theorem Multiset.nodup_cons

added theorem Multiset.nodup_iff_count_le_one

added theorem Multiset.nodup_iff_le

added theorem Multiset.nodup_iff_ne_cons_cons

added theorem Multiset.nodup_iff_pairwise

added theorem Multiset.nodup_map_iff_inj_on

added theorem Multiset.nodup_of_le

added theorem Multiset.nodup_range

added theorem Multiset.nodup_singleton

added theorem Multiset.nodup_union

added theorem Multiset.nodup_zero

added theorem Multiset.not_nodup_pair

added theorem Multiset.range_le