Commit 2023-01-11 16:31 c5a07b22

View on Github →

feat: port Mathlib.Data.List.Perm (#1478)

Estimated changes

Modified Mathlib/Data/List/Infix.lean

modified theorem List.infix_insert

modified theorem List.suffix_insert

Modified Mathlib/Data/List/Nodup.lean

added theorem List.Nodup.take_eq_filter_mem

Modified Mathlib/Data/List/Perm.lean

added theorem List.Nodup.sublist_ext

added theorem List.Pairwise.perm

deleted theorem List.Perm.Equivalence

added theorem List.Perm.append

added theorem List.Perm.append_cons

added theorem List.Perm.append_left

added theorem List.Perm.append_right

added theorem List.Perm.bag_inter

added theorem List.Perm.bag_inter_left

added theorem List.Perm.bag_inter_right

added theorem List.Perm.bind_left

added theorem List.Perm.bind_right

added theorem List.Perm.count_eq

added theorem List.Perm.countp_congr

added theorem List.Perm.countp_eq

added theorem List.Perm.dedup

added theorem List.Perm.diff

added theorem List.Perm.diff_left

added theorem List.Perm.diff_right

added theorem List.Perm.dropSlice_inter

added theorem List.Perm.drop_inter

modified theorem List.Perm.eq_nil

added theorem List.Perm.eq_singleton

added theorem List.Perm.eqv

added theorem List.Perm.erase

added theorem List.Perm.erasep

added theorem List.Perm.filter

added theorem List.Perm.filterMap

added theorem List.Perm.fold_op_eq

added theorem List.Perm.foldl_eq'

added theorem List.Perm.foldl_eq

added theorem List.Perm.foldr_eq

added theorem List.Perm.insert

added theorem List.Perm.inter

added theorem List.Perm.inter_append

added theorem List.Perm.inter_left

added theorem List.Perm.inter_right

added theorem List.Perm.join

added theorem List.Perm.join_congr

modified theorem List.Perm.length_eq

added theorem List.Perm.map

modified theorem List.Perm.nil_eq

added theorem List.Perm.of_eq

added theorem List.Perm.pairwise

added theorem List.Perm.permutations'

added theorem List.Perm.permutations

added theorem List.Perm.pmap

added theorem List.Perm.prod_eq'

added theorem List.Perm.prod_eq

added theorem List.Perm.product

added theorem List.Perm.product_left

added theorem List.Perm.product_right

added theorem List.Perm.rec_heq

added theorem List.Perm.singleton_eq

added theorem List.Perm.sizeOf_eq_sizeOf

added theorem List.Perm.subperm

added theorem List.Perm.subperm_left

added theorem List.Perm.subperm_right

modified theorem List.Perm.subset

modified theorem List.Perm.swap'

added theorem List.Perm.take_inter

added theorem List.Perm.union

added theorem List.Perm.union_left

added theorem List.Perm.union_right

modified inductive List.Perm

deleted theorem List.Perm_comm

added theorem List.Sublist.exists_perm_append

added theorem List.Sublist.subperm

added theorem List.Subperm.antisymm

added theorem List.Subperm.cons_left

added theorem List.Subperm.cons_right

added theorem List.Subperm.count_le

added theorem List.Subperm.countp_le

added theorem List.Subperm.diff_right

added theorem List.Subperm.erase

added theorem List.Subperm.exists_of_length_lt

added theorem List.Subperm.filter

added theorem List.Subperm.length_le

added theorem List.Subperm.perm_of_length_le

added theorem List.Subperm.refl

added theorem List.Subperm.subset

added theorem List.Subperm.trans

added def List.Subperm

added theorem List.bind_append_perm

added theorem List.concat_perm

added theorem List.cons_perm_iff_perm_erase

added theorem List.cons_subperm_of_mem

added theorem List.count_permutations'Aux_self

added theorem List.countp_eq_countp_filter_add

added theorem List.erase_cons_subperm_cons_erase

added theorem List.erase_subperm

added theorem List.exists_perm_sublist

added theorem List.filter_append_perm

added theorem List.forall₂_comp_perm_eq_perm_comp_forall₂

added theorem List.injective_permutations'Aux

added theorem List.length_permutations'Aux

added theorem List.length_permutations

added theorem List.length_permutationsAux

added theorem List.map_append_bind_perm

added theorem List.mem_permutations'

added theorem List.mem_permutations

added theorem List.mem_permutationsAux_of_perm

added theorem List.mem_permutations_of_perm_lemma

added theorem List.nil_perm

added theorem List.nil_subperm

added theorem List.nodup_permutations'Aux_iff

added theorem List.nodup_permutations'Aux_of_not_mem

added theorem List.nodup_permutations

added theorem List.not_perm_nil_cons

added theorem List.nthLe_permutations'Aux

added theorem List.perm_append_comm

added theorem List.perm_append_left_iff

added theorem List.perm_append_right_iff

added theorem List.perm_append_singleton

added theorem List.perm_comm

added theorem List.perm_comp_forall₂

added theorem List.perm_comp_perm

added theorem List.perm_cons

added theorem List.perm_cons_append_cons

added theorem List.perm_cons_erase

added theorem List.perm_ext

added theorem List.perm_iff_count

modified theorem List.perm_induction_on

modified theorem List.perm_insertNth

added theorem List.perm_insert_swap

added theorem List.perm_lookmap

modified theorem List.perm_middle

added theorem List.perm_nil

added theorem List.perm_of_mem_permutations

added theorem List.perm_of_mem_permutationsAux

added theorem List.perm_option_to_list

added theorem List.perm_permutations'Aux_comm

added theorem List.perm_permutations'_iff

added theorem List.perm_permutations_iff

added theorem List.perm_repeat

added theorem List.perm_replicate

added theorem List.perm_singleton

added theorem List.permutations'Aux_nthLe_zero

added theorem List.permutations_perm_permutations'

added theorem List.prod_reverse

added theorem List.rel_perm

added theorem List.rel_perm_imp

added theorem List.repeat_perm

added theorem List.replicate_perm

added theorem List.reverse_perm

added theorem List.singleton_perm

added theorem List.singleton_perm_singleton

added theorem List.subperm_append_diff_self_of_count_le

added theorem List.subperm_append_left

added theorem List.subperm_append_right

added theorem List.subperm_cons

added theorem List.subperm_cons_diff

added theorem List.subperm_cons_erase

added theorem List.subperm_ext_iff

added theorem List.subperm_singleton_iff

added theorem List.subset_cons_diff

Modified Mathlib/Data/Multiset/Basic.lean

modified def Multiset

Modified Mathlib/Init/Data/List/Lemmas.lean

Modified Mathlib/Testing/SlimCheck/Gen.lean