Commit 2023-01-10 18:23 ff1d0226

View on Github →

feat: port Mathlib.Data.List.Nodup (#1456)

Estimated changes

Modified Mathlib/Data/List/Nodup.lean

added theorem List.Nodup.append

added theorem List.Nodup.diff

added theorem List.Nodup.diff_eq_filter

added theorem List.Nodup.erase

added theorem List.Nodup.erase_eq_filter

added theorem List.Nodup.filter

added theorem List.Nodup.get_inj_iff

added theorem List.Nodup.insert

added theorem List.Nodup.inter

added theorem List.Nodup.map_update

added theorem List.Nodup.mem_diff_iff

added theorem List.Nodup.mem_erase_iff

added theorem List.Nodup.ne_singleton_iff

added theorem List.Nodup.not_mem

added theorem List.Nodup.not_mem_erase

added theorem List.Nodup.nthLe_inj_iff

added theorem List.Nodup.of_append_left

added theorem List.Nodup.of_append_right

added theorem List.Nodup.of_cons

added theorem List.Nodup.pairwise_coe

added theorem List.Nodup.pairwise_of_forall_ne

added theorem List.Nodup.pairwise_of_set_pairwise

added theorem List.Nodup.sigma

added theorem List.Nodup.union

added theorem List.count_eq_of_nodup

added theorem List.count_eq_one_of_mem

added theorem List.disjoint_of_nodup_append

added theorem List.forall_mem_ne

added theorem List.get_indexOf

added theorem List.inj_on_of_nodup_map

added theorem List.nodup_append

added theorem List.nodup_append_comm

added theorem List.nodup_bind

added theorem List.nodup_cons

added theorem List.nodup_iff_count_le_one

added theorem List.nodup_iff_get?_ne_get?

added theorem List.nodup_iff_injective_get

added theorem List.nodup_iff_nthLe_inj

added theorem List.nodup_iff_sublist

added theorem List.nodup_join

added theorem List.nodup_map_iff

added theorem List.nodup_map_iff_inj_on

added theorem List.nodup_middle

added theorem List.nodup_nil

added theorem List.nodup_repeat

added theorem List.nodup_replicate

added theorem List.nodup_reverse

added theorem List.nodup_singleton

added theorem List.not_nodup_cons_of_mem

added theorem List.not_nodup_of_get_eq_of_ne

added theorem List.not_nodup_pair

added theorem List.nthLe_eq_of_ne_imp_not_nodup

added theorem List.nthLe_index_of

added theorem List.rel_nodup

added theorem Option.toList_nodup

Modified Mathlib/Data/List/Pairwise.lean

modified theorem List.Pairwise.filter