Commit 2023-01-10 21:18 3ca4b32c

View on Github →

feat: port Mathlib.Data.List.Dedup (#1460)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Dedup.lean

added theorem List.count_dedup

added theorem List.dedup_append

added theorem List.dedup_cons_of_mem'

added theorem List.dedup_cons_of_mem

added theorem List.dedup_cons_of_not_mem'

added theorem List.dedup_cons_of_not_mem

added theorem List.dedup_eq_self

added theorem List.dedup_idempotent

added theorem List.dedup_nil

added theorem List.dedup_sublist

added theorem List.dedup_subset

added theorem List.mem_dedup

added theorem List.nodup_dedup

added theorem List.repeat_dedup

added theorem List.replicate_dedup

added theorem List.subset_dedup

added theorem List.sum_map_count_dedup_eq_length

added theorem List.sum_map_count_dedup_filter_eq_countp