Documentation

Mathlib.Data.Multiset.Dedup

Erasing duplicates in a multiset. #

dedup #

def Multiset.dedup {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) :

dedup s removes duplicates from s, yielding a nodup multiset.

Equations
@[simp]
theorem Multiset.coe_dedup {α : Type u_1} [inst : DecidableEq α] (l : List α) :
@[simp]
theorem Multiset.dedup_zero {α : Type u_1} [inst : DecidableEq α] :
@[simp]
theorem Multiset.mem_dedup {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :
@[simp]
theorem Multiset.dedup_cons_of_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :
@[simp]
theorem Multiset.dedup_cons_of_not_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} :
theorem Multiset.dedup_le {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) :
theorem Multiset.dedup_subset {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) :
theorem Multiset.subset_dedup {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) :
@[simp]
theorem Multiset.dedup_subset' {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :
@[simp]
theorem Multiset.subset_dedup' {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :
@[simp]
theorem Multiset.nodup_dedup {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) :
theorem Multiset.Nodup.dedup {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} :

Alias of the reverse direction of Multiset.dedup_eq_self.

theorem Multiset.count_dedup {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (a : α) :
Multiset.count a (Multiset.dedup m) = if a m then 1 else 0
@[simp]
theorem Multiset.dedup_bind_dedup {α : Type u_2} {β : Type u_1} [inst : DecidableEq α] [inst : DecidableEq β] (m : Multiset α) (f : αMultiset β) :
theorem Multiset.dedup_eq_zero {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} :
@[simp]
theorem Multiset.dedup_singleton {α : Type u_1} [inst : DecidableEq α] {a : α} :
theorem Multiset.le_dedup {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :
theorem Multiset.dedup_ext {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} :
Multiset.dedup s = Multiset.dedup t ∀ (a : α), a s a t
theorem Multiset.dedup_map_dedup_eq {α : Type u_2} {β : Type u_1} [inst : DecidableEq α] [inst : DecidableEq β] (f : αβ) (s : Multiset α) :
@[simp]
theorem Multiset.dedup_nsmul {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {n : } (h0 : n 0) :
theorem Multiset.Nodup.le_dedup_iff_le {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} {t : Multiset α} (hno : Multiset.Nodup s) :
theorem Multiset.Nodup.le_nsmul_iff_le {α : Type u_1} {s : Multiset α} {t : Multiset α} {n : } (h : Multiset.Nodup s) (hn : n 0) :
s n t s t