Documentation

Mathlib.Data.List.Dedup

Erasure of duplicates in a list #

This file proves basic results about List.dedup (definition in Data.List.Defs). dedup l returns l without its duplicates. It keeps the earliest (that is, rightmost) occurrence of each.

Tags #

duplicate, multiplicity, nodup, nub

@[simp]
theorem List.dedup_nil {α : Type u} [DecidableEq α] :
theorem List.dedup_cons_of_mem' {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a List.dedup l) :
theorem List.dedup_cons_of_not_mem' {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : ¬a List.dedup l) :
@[simp]
theorem List.mem_dedup {α : Type u} [DecidableEq α] {a : α} {l : List α} :
@[simp]
theorem List.dedup_cons_of_mem {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a l) :
@[simp]
theorem List.dedup_cons_of_not_mem {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : ¬a l) :
theorem List.dedup_subset {α : Type u} [DecidableEq α] (l : List α) :
theorem List.subset_dedup {α : Type u} [DecidableEq α] (l : List α) :
theorem List.nodup_dedup {α : Type u} [DecidableEq α] (l : List α) :
theorem List.dedup_eq_self {α : Type u} [DecidableEq α] {l : List α} :
theorem List.dedup_eq_cons {α : Type u} [DecidableEq α] (l : List α) (a : α) (l' : List α) :
@[simp]
theorem List.dedup_eq_nil {α : Type u} [DecidableEq α] (l : List α) :
List.dedup l = [] l = []
theorem List.Nodup.dedup {α : Type u} [DecidableEq α] {l : List α} (h : List.Nodup l) :
@[simp]
theorem List.dedup_idem {α : Type u} [DecidableEq α] {l : List α} :
theorem List.dedup_append {α : Type u} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
List.dedup (l₁ ++ l₂) = l₁ List.dedup l₂
theorem List.replicate_dedup {α : Type u} [DecidableEq α] {x : α} {k : } :
k 0List.dedup (List.replicate k x) = [x]
theorem List.count_dedup {α : Type u} [DecidableEq α] (l : List α) (a : α) :
List.count a (List.dedup l) = if a l then 1 else 0
theorem List.sum_map_count_dedup_filter_eq_countP {α : Type u} [DecidableEq α] (p : αBool) (l : List α) :

Summing the count of x over a list filtered by some p is just countP applied to p