Commit 2023-01-10 20:53 b5ff35f9

View on Github →

feat: port Mathlib.Data.List.Duplicate (#1465)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Duplicate.lean

added theorem List.Duplicate.duplicate_cons

added theorem List.Duplicate.elim_nil

added theorem List.Duplicate.elim_singleton

added theorem List.Duplicate.mem

added theorem List.Duplicate.mem_cons_self

added theorem List.Duplicate.mono_sublist

added theorem List.Duplicate.ne_nil

added theorem List.Duplicate.ne_singleton

added theorem List.Duplicate.not_nodup

added theorem List.Duplicate.of_duplicate_cons

added inductive List.Duplicate

added theorem List.Mem.duplicate_cons_self

added theorem List.duplicate_cons_iff

added theorem List.duplicate_cons_iff_of_ne

added theorem List.duplicate_cons_self_iff

added theorem List.duplicate_iff_sublist

added theorem List.duplicate_iff_two_le_count

added theorem List.exists_duplicate_iff_not_nodup

added theorem List.nodup_iff_forall_not_duplicate

added theorem List.not_duplicate_nil

added theorem List.not_duplicate_singleton