Erasing duplicates in a multiset. #
dedup #
dedup s
removes duplicates from s
, yielding a nodup
multiset.
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Alias of the reverse direction of multiset.dedup_eq_self
.
@[simp]
theorem
multiset.dedup_map_dedup_eq
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
(f : α → β)
(s : multiset α) :
(multiset.map f s.dedup).dedup = (multiset.map f s).dedup
@[simp]
theorem
multiset.dedup_nsmul
{α : Type u_1}
[decidable_eq α]
{s : multiset α}
{n : ℕ}
(h0 : n ≠ 0) :
theorem
multiset.nodup.le_dedup_iff_le
{α : Type u_1}
[decidable_eq α]
{s t : multiset α}
(hno : s.nodup) :