Erasing duplicates in a multiset.
erase_dup
erase_dup s removes duplicates from s, yielding a nodup multiset.
@[simp]
@[simp]
@[simp]
@[simp]
theorem
multiset.erase_dup_cons_of_not_mem
{α : Type u_1}
[decidable_eq α]
{a : α}
{s : multiset α} :
@[simp]
@[simp]
@[simp]
@[simp]
theorem
multiset.erase_dup_map_erase_dup_eq
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
(f : α → β)
(s : multiset α) :
(multiset.map f s.erase_dup).erase_dup = (multiset.map f s).erase_dup