# 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} [] :
= []
theorem List.dedup_cons_of_mem' {α : Type u} [] {a : α} {l : List α} (h : a ) :
List.dedup (a :: l) =
theorem List.dedup_cons_of_not_mem' {α : Type u} [] {a : α} {l : List α} (h : ¬a ) :
List.dedup (a :: l) = a ::
@[simp]
theorem List.mem_dedup {α : Type u} [] {a : α} {l : List α} :
a a l
@[simp]
theorem List.dedup_cons_of_mem {α : Type u} [] {a : α} {l : List α} (h : a l) :
List.dedup (a :: l) =
@[simp]
theorem List.dedup_cons_of_not_mem {α : Type u} [] {a : α} {l : List α} (h : ¬a l) :
List.dedup (a :: l) = a ::
theorem List.dedup_sublist {α : Type u} [] (l : List α) :
theorem List.dedup_subset {α : Type u} [] (l : List α) :
l
theorem List.subset_dedup {α : Type u} [] (l : List α) :
l
theorem List.nodup_dedup {α : Type u} [] (l : List α) :
theorem List.headI_dedup {α : Type u} [] [] (l : List α) :
= if then else
theorem List.tail_dedup {α : Type u} [] [] (l : List α) :
= if then List.tail () else
theorem List.dedup_eq_self {α : Type u} [] {l : List α} :
= l
theorem List.dedup_eq_cons {α : Type u} [] (l : List α) (a : α) (l' : List α) :
= a :: l' a l ¬a l' = l'
@[simp]
theorem List.dedup_eq_nil {α : Type u} [] (l : List α) :
= [] l = []
theorem List.Nodup.dedup {α : Type u} [] {l : List α} (h : ) :
= l
@[simp]
theorem List.dedup_idem {α : Type u} [] {l : List α} :
theorem List.dedup_append {α : Type u} [] (l₁ : List α) (l₂ : List α) :
List.dedup (l₁ ++ l₂) = l₁
theorem List.replicate_dedup {α : Type u} [] {x : α} {k : } :
k 0List.dedup () = [x]
theorem List.count_dedup {α : Type u} [] (l : List α) (a : α) :
List.count a () = if a l then 1 else 0
theorem List.sum_map_count_dedup_filter_eq_countP {α : Type u} [] (p : αBool) (l : List α) :
List.sum (List.map (fun x => ) ()) =

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

theorem List.sum_map_count_dedup_eq_length {α : Type u} [] (l : List α) :
List.sum (List.map (fun x => ) ()) =