Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-09 02:50 fbc95927

View on Github →

chore(data/list): move some sections to separate files (#2341)

move list.func namespace to its own file
move erase_dup to its own file
move rotate to its own file
move tfae to its own file
move bag_inter and intervals
move range out
move nodup
move chain and pairwise
move zip
move forall2
move of_fn
add copyright headers
remove unnecessary sections, move defns to func.set and tfae
fixes
oops, forgot to add file

Estimated changes

Modified src/category/traversable/instances.lean

Modified src/data/int/basic.lean

Created src/data/list/antidiagonal.lean

added def list.nat.antidiagonal

added theorem list.nat.antidiagonal_zero

added theorem list.nat.length_antidiagonal

added theorem list.nat.mem_antidiagonal

added theorem list.nat.nodup_antidiagonal

Created src/data/list/bag_inter.lean

added theorem list.bag_inter_nil

added theorem list.bag_inter_nil_iff_inter_nil

added theorem list.bag_inter_sublist_left

added theorem list.cons_bag_inter_of_neg

added theorem list.cons_bag_inter_of_pos

added theorem list.count_bag_inter

added theorem list.mem_bag_inter

added theorem list.nil_bag_inter

Modified src/data/list/basic.lean

deleted theorem list.Ico.append_consecutive

deleted theorem list.Ico.bag_inter_consecutive

deleted theorem list.Ico.chain'_succ

deleted theorem list.Ico.eq_cons

deleted theorem list.Ico.eq_empty_iff

deleted theorem list.Ico.eq_nil_of_le

deleted theorem list.Ico.filter_le

deleted theorem list.Ico.filter_le_of_le

deleted theorem list.Ico.filter_le_of_le_bot

deleted theorem list.Ico.filter_le_of_top_le

deleted theorem list.Ico.filter_lt

deleted theorem list.Ico.filter_lt_of_ge

deleted theorem list.Ico.filter_lt_of_le_bot

deleted theorem list.Ico.filter_lt_of_top_le

deleted theorem list.Ico.inter_consecutive

deleted theorem list.Ico.length

deleted theorem list.Ico.map_add

deleted theorem list.Ico.map_sub

deleted theorem list.Ico.mem

deleted theorem list.Ico.nodup

deleted theorem list.Ico.not_mem_top

deleted theorem list.Ico.pairwise_lt

deleted theorem list.Ico.pred_singleton

deleted theorem list.Ico.self_empty

deleted theorem list.Ico.succ_singleton

deleted theorem list.Ico.succ_top

deleted theorem list.Ico.trichotomy

deleted theorem list.Ico.zero_bot

deleted def list.Ico

deleted theorem list.array_eq_of_fn

deleted theorem list.bag_inter_nil

deleted theorem list.bag_inter_nil_iff_inter_nil

deleted theorem list.bag_inter_sublist_left

deleted theorem list.bi_unique_forall₂

deleted theorem list.chain'.cons

deleted theorem list.chain'.iff

deleted theorem list.chain'.iff_mem

deleted theorem list.chain'.imp

deleted theorem list.chain'.tail

deleted theorem list.chain'_cons

deleted theorem list.chain'_iff_pairwise

deleted theorem list.chain'_map

deleted theorem list.chain'_map_of_chain'

deleted theorem list.chain'_nil

deleted theorem list.chain'_of_chain'_map

deleted theorem list.chain'_pair

deleted theorem list.chain'_reverse

deleted theorem list.chain'_singleton

deleted theorem list.chain'_split

deleted theorem list.chain.iff

deleted theorem list.chain.iff_mem

deleted theorem list.chain.imp'

deleted theorem list.chain.imp

deleted theorem list.chain_iff_pairwise

deleted theorem list.chain_lt_range'

deleted theorem list.chain_map

deleted theorem list.chain_map_of_chain

deleted theorem list.chain_of_chain_cons

deleted theorem list.chain_of_chain_map

deleted theorem list.chain_of_pairwise

deleted theorem list.chain_singleton

deleted theorem list.chain_split

deleted theorem list.chain_succ_range'

deleted theorem list.cons_bag_inter_of_neg

deleted theorem list.cons_bag_inter_of_pos

deleted theorem list.count_bag_inter

deleted theorem list.count_eq_one_of_mem

deleted theorem list.diff_eq_filter_of_nodup

deleted theorem list.disjoint_of_nodup_append

deleted theorem list.enum_from_map_fst

deleted theorem list.enum_map_fst

deleted theorem list.erase_dup_append

deleted theorem list.erase_dup_cons_of_mem'

deleted theorem list.erase_dup_cons_of_mem

deleted theorem list.erase_dup_cons_of_not_mem'

deleted theorem list.erase_dup_cons_of_not_mem

deleted theorem list.erase_dup_eq_self

deleted theorem list.erase_dup_idempotent

deleted theorem list.erase_dup_nil

deleted theorem list.erase_dup_sublist

deleted theorem list.erase_dup_subset

deleted theorem list.filter_map_cons

deleted def list.fin_range

deleted theorem list.forall_mem_ne

deleted theorem list.forall_mem_pw_filter

deleted theorem list.forall_of_forall_of_pairwise

deleted theorem list.forall_of_pairwise

deleted theorem list.forall₂.flip

deleted theorem list.forall₂.imp

deleted theorem list.forall₂.mp

deleted theorem list.forall₂_and_left

deleted theorem list.forall₂_cons

deleted theorem list.forall₂_cons_left_iff

deleted theorem list.forall₂_cons_right_iff

deleted theorem list.forall₂_drop

deleted theorem list.forall₂_drop_append

deleted theorem list.forall₂_eq_eq_eq

deleted theorem list.forall₂_iff_zip

deleted theorem list.forall₂_length_eq

deleted theorem list.forall₂_map_left_iff

deleted theorem list.forall₂_map_right_iff

deleted theorem list.forall₂_nil_left_iff

deleted theorem list.forall₂_nil_right_iff

deleted theorem list.forall₂_refl

deleted theorem list.forall₂_same

deleted theorem list.forall₂_take

deleted theorem list.forall₂_take_append

deleted theorem list.forall₂_zip

deleted theorem list.func.add_nil

deleted theorem list.func.eq_get_of_mem

deleted theorem list.func.eq_of_equiv

deleted theorem list.func.equiv_of_eq

deleted theorem list.func.equiv_refl

deleted theorem list.func.equiv_symm

deleted theorem list.func.equiv_trans

deleted theorem list.func.forall_val_of_forall_mem

deleted theorem list.func.get_add

deleted theorem list.func.get_eq_default_of_le

deleted theorem list.func.get_map'

deleted theorem list.func.get_map

deleted theorem list.func.get_neg

deleted theorem list.func.get_nil

deleted theorem list.func.get_pointwise

deleted theorem list.func.get_set

deleted theorem list.func.get_set_eq_of_ne

deleted theorem list.func.get_sub

deleted theorem list.func.length_add

deleted theorem list.func.length_neg

deleted theorem list.func.length_pointwise

deleted theorem list.func.length_set

deleted theorem list.func.length_sub

deleted theorem list.func.map_add_map

deleted theorem list.func.mem_get_of_le

deleted theorem list.func.mem_get_of_ne_zero

deleted theorem list.func.nil_add

deleted theorem list.func.nil_pointwise

deleted theorem list.func.nil_sub

deleted theorem list.func.pointwise_nil

deleted theorem list.func.sub_nil

deleted theorem list.iota_eq_reverse_range'

deleted theorem list.left_unique_forall₂

deleted theorem list.length_fin_range

deleted theorem list.length_iota

deleted theorem list.length_of_fn

deleted theorem list.length_of_fn_aux

deleted theorem list.length_range'

deleted theorem list.length_range

deleted theorem list.length_revzip

deleted theorem list.length_rotate'

deleted theorem list.length_rotate

deleted theorem list.length_zip

deleted theorem list.map_add_range'

deleted theorem list.map_sub_range'

deleted theorem list.mem_bag_inter

deleted theorem list.mem_diff_iff_of_nodup

deleted theorem list.mem_erase_dup

deleted theorem list.mem_erase_iff_of_nodup

deleted theorem list.mem_erase_of_nodup

deleted theorem list.mem_fin_range

deleted theorem list.mem_iota

deleted theorem list.mem_range'

deleted theorem list.mem_range

deleted theorem list.mem_rotate

deleted theorem list.mem_sections

deleted theorem list.mem_sections_length

deleted theorem list.mem_zip

deleted def list.nat.antidiagonal

deleted theorem list.nat.antidiagonal_zero

deleted theorem list.nat.length_antidiagonal

deleted theorem list.nat.mem_antidiagonal

deleted theorem list.nat.nodup_antidiagonal

deleted theorem list.nil_bag_inter

deleted theorem list.nodup_append

deleted theorem list.nodup_append_comm

deleted theorem list.nodup_append_of_nodup

deleted theorem list.nodup_attach

deleted theorem list.nodup_bind

deleted theorem list.nodup_concat

deleted theorem list.nodup_cons

deleted theorem list.nodup_cons_of_nodup

deleted theorem list.nodup_diff

deleted theorem list.nodup_erase_dup

deleted theorem list.nodup_erase_eq_filter

deleted theorem list.nodup_erase_of_nodup

deleted theorem list.nodup_filter

deleted theorem list.nodup_filter_map

deleted theorem list.nodup_fin_range

deleted theorem list.nodup_iff_count_le_one

deleted theorem list.nodup_iff_nth_le_inj

deleted theorem list.nodup_iff_sublist

deleted theorem list.nodup_insert

deleted theorem list.nodup_inter_of_nodup

deleted theorem list.nodup_iota

deleted theorem list.nodup_join

deleted theorem list.nodup_map

deleted theorem list.nodup_map_iff

deleted theorem list.nodup_map_on

deleted theorem list.nodup_middle

deleted theorem list.nodup_nil

deleted theorem list.nodup_of_fn

deleted theorem list.nodup_of_nodup_append_left

deleted theorem list.nodup_of_nodup_append_right

deleted theorem list.nodup_of_nodup_cons

deleted theorem list.nodup_of_nodup_map

deleted theorem list.nodup_of_sublist

deleted theorem list.nodup_pmap

deleted theorem list.nodup_product

deleted theorem list.nodup_range'

deleted theorem list.nodup_range

deleted theorem list.nodup_repeat

deleted theorem list.nodup_reverse

deleted theorem list.nodup_sigma

deleted theorem list.nodup_singleton

deleted theorem list.nodup_sublists'

deleted theorem list.nodup_sublists

deleted theorem list.nodup_sublists_len

deleted theorem list.nodup_union

deleted theorem list.nodup_update_nth

deleted theorem list.not_mem_of_nodup_cons

deleted theorem list.not_mem_range_self

deleted theorem list.not_nodup_cons_of_mem

deleted theorem list.not_nodup_pair

deleted theorem list.nth_le_index_of

deleted theorem list.nth_le_of_fn

deleted theorem list.nth_le_range

deleted theorem list.nth_of_fn

deleted theorem list.nth_of_fn_aux

deleted theorem list.nth_range'

deleted theorem list.nth_range

deleted theorem list.of_fn_eq_pmap

deleted theorem list.of_fn_nth_le

deleted theorem list.of_fn_succ

deleted theorem list.of_fn_zero

deleted theorem list.pairwise.and

deleted theorem list.pairwise.and_mem

deleted theorem list.pairwise.chain'

deleted theorem list.pairwise.iff

deleted theorem list.pairwise.iff_of_mem

deleted theorem list.pairwise.imp

deleted theorem list.pairwise.imp_mem

deleted theorem list.pairwise.imp_of_mem

deleted theorem list.pairwise.imp₂

deleted theorem list.pairwise_append

deleted theorem list.pairwise_append_comm

deleted theorem list.pairwise_filter

deleted theorem list.pairwise_filter_map

deleted theorem list.pairwise_filter_map_of_pairwise

deleted theorem list.pairwise_filter_of_pairwise

deleted theorem list.pairwise_gt_iota

deleted theorem list.pairwise_iff_nth_le

deleted theorem list.pairwise_join

deleted theorem list.pairwise_lt_range'

deleted theorem list.pairwise_lt_range

deleted theorem list.pairwise_map

deleted theorem list.pairwise_map_of_pairwise

deleted theorem list.pairwise_middle

deleted theorem list.pairwise_of_forall

deleted theorem list.pairwise_of_pairwise_cons

deleted theorem list.pairwise_of_pairwise_map

deleted theorem list.pairwise_of_sublist

deleted theorem list.pairwise_pair

deleted theorem list.pairwise_pw_filter

deleted theorem list.pairwise_reverse

deleted theorem list.pairwise_singleton

deleted theorem list.pairwise_sublists'

deleted theorem list.pairwise_sublists

deleted theorem list.prod_range_succ

deleted theorem list.prod_rotate_eq_one_of_prod_eq_one

deleted theorem list.pw_filter_cons_of_neg

deleted theorem list.pw_filter_cons_of_pos

deleted theorem list.pw_filter_eq_self

deleted theorem list.pw_filter_idempotent

deleted theorem list.pw_filter_map

deleted theorem list.pw_filter_nil

deleted theorem list.pw_filter_sublist

deleted theorem list.pw_filter_subset

deleted theorem list.range'_append

deleted theorem list.range'_concat

deleted theorem list.range'_eq_map_range

deleted theorem list.range'_sublist_right

deleted theorem list.range'_subset_right

deleted theorem list.range_concat

deleted theorem list.range_core_range'

deleted theorem list.range_eq_range'

deleted theorem list.range_sublist

deleted theorem list.range_subset

deleted theorem list.range_succ_eq_map

deleted theorem list.rel_append

deleted theorem list.rel_bind

deleted theorem list.rel_filter

deleted theorem list.rel_filter_map

deleted theorem list.rel_foldl

deleted theorem list.rel_foldr

deleted theorem list.rel_join

deleted theorem list.rel_map

deleted theorem list.rel_mem

deleted theorem list.rel_nodup

deleted theorem list.rel_of_chain_cons

deleted theorem list.rel_of_pairwise_cons

deleted theorem list.rel_prod

deleted theorem list.rel_sections

deleted theorem list.reverse_range'

deleted theorem list.reverse_revzip

deleted theorem list.revzip_map_fst

deleted theorem list.revzip_map_snd

deleted theorem list.revzip_swap

deleted theorem list.right_unique_forall₂

deleted theorem list.rotate'_cons_succ

deleted theorem list.rotate'_eq_take_append_drop

deleted theorem list.rotate'_length

deleted theorem list.rotate'_length_mul

deleted theorem list.rotate'_mod

deleted theorem list.rotate'_nil

deleted theorem list.rotate'_rotate'

deleted theorem list.rotate'_zero

deleted theorem list.rotate_cons_succ

deleted theorem list.rotate_eq_rotate'

deleted theorem list.rotate_eq_take_append_drop

deleted theorem list.rotate_length

deleted theorem list.rotate_length_mul

deleted theorem list.rotate_mod

deleted theorem list.rotate_nil

deleted theorem list.rotate_rotate

deleted theorem list.rotate_zero

deleted theorem list.subset_erase_dup

deleted theorem list.tfae.out

deleted theorem list.tfae_cons_cons

deleted theorem list.tfae_cons_of_mem

deleted theorem list.tfae_nil

deleted theorem list.tfae_of_cycle

deleted theorem list.tfae_of_forall

deleted theorem list.tfae_singleton

deleted theorem list.unzip_cons

deleted theorem list.unzip_eq_map

deleted theorem list.unzip_left

deleted theorem list.unzip_nil

deleted theorem list.unzip_revzip

deleted theorem list.unzip_right

deleted theorem list.unzip_swap

deleted theorem list.unzip_zip

deleted theorem list.unzip_zip_left

deleted theorem list.unzip_zip_right

deleted theorem list.zip_append

deleted theorem list.zip_cons_cons

deleted theorem list.zip_map'

deleted theorem list.zip_map

deleted theorem list.zip_map_left

deleted theorem list.zip_map_right

deleted theorem list.zip_nil_left

deleted theorem list.zip_nil_right

deleted theorem list.zip_swap

deleted theorem list.zip_unzip

deleted theorem option.to_list_nodup

Created src/data/list/chain.lean

added theorem list.chain'.cons

added theorem list.chain'.iff

added theorem list.chain'.iff_mem

added theorem list.chain'.imp

added theorem list.chain'.tail

added theorem list.chain'_cons

added theorem list.chain'_iff_pairwise

added theorem list.chain'_map

added theorem list.chain'_map_of_chain'

added theorem list.chain'_nil

added theorem list.chain'_of_chain'_map

added theorem list.chain'_pair

added theorem list.chain'_reverse

added theorem list.chain'_singleton

added theorem list.chain'_split

added theorem list.chain.iff

added theorem list.chain.iff_mem

added theorem list.chain.imp'

added theorem list.chain.imp

added theorem list.chain_iff_pairwise

added theorem list.chain_map

added theorem list.chain_map_of_chain

added theorem list.chain_of_chain_cons

added theorem list.chain_of_chain_map

added theorem list.chain_of_pairwise

added theorem list.chain_singleton

added theorem list.chain_split

added theorem list.pairwise.chain'

added theorem list.rel_of_chain_cons

Modified src/data/list/defs.lean

deleted def list.func.add

deleted def list.func.equiv

deleted def list.func.get

deleted def list.func.neg

deleted def list.func.pointwise

deleted def list.func.set

deleted def list.func.sub

deleted def list.tfae

Created src/data/list/erase_dup.lean

added theorem list.erase_dup_append

added theorem list.erase_dup_cons_of_mem'

added theorem list.erase_dup_cons_of_mem

added theorem list.erase_dup_cons_of_not_mem'

added theorem list.erase_dup_cons_of_not_mem

added theorem list.erase_dup_eq_self

added theorem list.erase_dup_idempotent

added theorem list.erase_dup_nil

added theorem list.erase_dup_sublist

added theorem list.erase_dup_subset

added theorem list.mem_erase_dup

added theorem list.nodup_erase_dup

added theorem list.subset_erase_dup

Created src/data/list/forall2.lean

added theorem list.bi_unique_forall₂

added theorem list.filter_map_cons

added theorem list.forall₂.flip

added theorem list.forall₂.imp

added theorem list.forall₂.mp

added theorem list.forall₂_and_left

added theorem list.forall₂_cons

added theorem list.forall₂_cons_left_iff

added theorem list.forall₂_cons_right_iff

added theorem list.forall₂_drop

added theorem list.forall₂_drop_append

added theorem list.forall₂_eq_eq_eq

added theorem list.forall₂_iff_zip

added theorem list.forall₂_length_eq

added theorem list.forall₂_map_left_iff

added theorem list.forall₂_map_right_iff

added theorem list.forall₂_nil_left_iff

added theorem list.forall₂_nil_right_iff

added theorem list.forall₂_refl

added theorem list.forall₂_same

added theorem list.forall₂_take

added theorem list.forall₂_take_append

added theorem list.forall₂_zip

added theorem list.left_unique_forall₂

added theorem list.rel_append

added theorem list.rel_bind

added theorem list.rel_filter

added theorem list.rel_filter_map

added theorem list.rel_foldl

added theorem list.rel_foldr

added theorem list.rel_join

added theorem list.rel_map

added theorem list.rel_mem

added theorem list.rel_prod

added theorem list.right_unique_forall₂

Created src/data/list/func.lean

added def list.func.add

added theorem list.func.add_nil

added theorem list.func.eq_get_of_mem

added theorem list.func.eq_of_equiv

added def list.func.equiv

added theorem list.func.equiv_of_eq

added theorem list.func.equiv_refl

added theorem list.func.equiv_symm

added theorem list.func.equiv_trans

added theorem list.func.forall_val_of_forall_mem

added def list.func.get

added theorem list.func.get_add

added theorem list.func.get_eq_default_of_le

added theorem list.func.get_map'

added theorem list.func.get_map

added theorem list.func.get_neg

added theorem list.func.get_nil

added theorem list.func.get_pointwise

added theorem list.func.get_set

added theorem list.func.get_set_eq_of_ne

added theorem list.func.get_sub

added theorem list.func.length_add

added theorem list.func.length_neg

added theorem list.func.length_pointwise

added theorem list.func.length_set

added theorem list.func.length_sub

added theorem list.func.map_add_map

added theorem list.func.mem_get_of_le

added theorem list.func.mem_get_of_ne_zero

added def list.func.neg

added theorem list.func.nil_add

added theorem list.func.nil_pointwise

added theorem list.func.nil_sub

added def list.func.pointwise

added theorem list.func.pointwise_nil

added def list.func.set

added def list.func.sub

added theorem list.func.sub_nil

Created src/data/list/intervals.lean

added theorem list.Ico.append_consecutive

added theorem list.Ico.bag_inter_consecutive

added theorem list.Ico.chain'_succ

added theorem list.Ico.eq_cons

added theorem list.Ico.eq_empty_iff

added theorem list.Ico.eq_nil_of_le

added theorem list.Ico.filter_le

added theorem list.Ico.filter_le_of_le

added theorem list.Ico.filter_le_of_le_bot

added theorem list.Ico.filter_le_of_top_le

added theorem list.Ico.filter_lt

added theorem list.Ico.filter_lt_of_ge

added theorem list.Ico.filter_lt_of_le_bot

added theorem list.Ico.filter_lt_of_top_le

added theorem list.Ico.inter_consecutive

added theorem list.Ico.length

added theorem list.Ico.map_add

added theorem list.Ico.map_sub

added theorem list.Ico.mem

added theorem list.Ico.nodup

added theorem list.Ico.not_mem_top

added theorem list.Ico.pairwise_lt

added theorem list.Ico.pred_singleton

added theorem list.Ico.self_empty

added theorem list.Ico.succ_singleton

added theorem list.Ico.succ_top

added theorem list.Ico.trichotomy

added theorem list.Ico.zero_bot

added def list.Ico

Created src/data/list/nodup.lean

added theorem list.count_eq_one_of_mem

added theorem list.diff_eq_filter_of_nodup

added theorem list.disjoint_of_nodup_append

added theorem list.forall_mem_ne

added theorem list.mem_diff_iff_of_nodup

added theorem list.mem_erase_iff_of_nodup

added theorem list.mem_erase_of_nodup

added theorem list.nodup_append

added theorem list.nodup_append_comm

added theorem list.nodup_append_of_nodup

added theorem list.nodup_attach

added theorem list.nodup_bind

added theorem list.nodup_concat

added theorem list.nodup_cons

added theorem list.nodup_cons_of_nodup

added theorem list.nodup_diff

added theorem list.nodup_erase_eq_filter

added theorem list.nodup_erase_of_nodup

added theorem list.nodup_filter

added theorem list.nodup_filter_map

added theorem list.nodup_iff_count_le_one

added theorem list.nodup_iff_nth_le_inj

added theorem list.nodup_iff_sublist

added theorem list.nodup_insert

added theorem list.nodup_inter_of_nodup

added theorem list.nodup_join

added theorem list.nodup_map

added theorem list.nodup_map_iff

added theorem list.nodup_map_on

added theorem list.nodup_middle

added theorem list.nodup_nil

added theorem list.nodup_of_nodup_append_left

added theorem list.nodup_of_nodup_append_right

added theorem list.nodup_of_nodup_cons

added theorem list.nodup_of_nodup_map

added theorem list.nodup_of_sublist

added theorem list.nodup_pmap

added theorem list.nodup_product

added theorem list.nodup_repeat

added theorem list.nodup_reverse

added theorem list.nodup_sigma

added theorem list.nodup_singleton

added theorem list.nodup_sublists'

added theorem list.nodup_sublists

added theorem list.nodup_sublists_len

added theorem list.nodup_union

added theorem list.nodup_update_nth

added theorem list.not_mem_of_nodup_cons

added theorem list.not_nodup_cons_of_mem

added theorem list.not_nodup_pair

added theorem list.nth_le_index_of

added theorem list.rel_nodup

added theorem option.to_list_nodup

Created src/data/list/of_fn.lean

added theorem list.array_eq_of_fn

added theorem list.length_of_fn

added theorem list.length_of_fn_aux

added theorem list.nth_le_of_fn

added theorem list.nth_of_fn

added theorem list.nth_of_fn_aux

added theorem list.of_fn_nth_le

added theorem list.of_fn_succ

added theorem list.of_fn_zero

Created src/data/list/pairwise.lean

added theorem list.forall_mem_pw_filter

added theorem list.forall_of_forall_of_pairwise

added theorem list.forall_of_pairwise

added theorem list.pairwise.and

added theorem list.pairwise.and_mem

added theorem list.pairwise.iff

added theorem list.pairwise.iff_of_mem

added theorem list.pairwise.imp

added theorem list.pairwise.imp_mem

added theorem list.pairwise.imp_of_mem

added theorem list.pairwise.imp₂

added theorem list.pairwise_append

added theorem list.pairwise_append_comm

added theorem list.pairwise_filter

added theorem list.pairwise_filter_map

added theorem list.pairwise_filter_map_of_pairwise

added theorem list.pairwise_filter_of_pairwise

added theorem list.pairwise_iff_nth_le

added theorem list.pairwise_join

added theorem list.pairwise_map

added theorem list.pairwise_map_of_pairwise

added theorem list.pairwise_middle

added theorem list.pairwise_of_forall

added theorem list.pairwise_of_pairwise_cons

added theorem list.pairwise_of_pairwise_map

added theorem list.pairwise_of_sublist

added theorem list.pairwise_pair

added theorem list.pairwise_pw_filter

added theorem list.pairwise_reverse

added theorem list.pairwise_singleton

added theorem list.pairwise_sublists'

added theorem list.pairwise_sublists

added theorem list.pw_filter_cons_of_neg

added theorem list.pw_filter_cons_of_pos

added theorem list.pw_filter_eq_self

added theorem list.pw_filter_idempotent

added theorem list.pw_filter_map

added theorem list.pw_filter_nil

added theorem list.pw_filter_sublist

added theorem list.pw_filter_subset

added theorem list.rel_of_pairwise_cons

Modified src/data/list/perm.lean

Created src/data/list/range.lean

added theorem list.chain_lt_range'

added theorem list.chain_succ_range'

added theorem list.enum_from_map_fst

added theorem list.enum_map_fst

added def list.fin_range

added theorem list.iota_eq_reverse_range'

added theorem list.length_fin_range

added theorem list.length_iota

added theorem list.length_range'

added theorem list.length_range

added theorem list.map_add_range'

added theorem list.map_sub_range'

added theorem list.mem_fin_range

added theorem list.mem_iota

added theorem list.mem_range'

added theorem list.mem_range

added theorem list.nodup_fin_range

added theorem list.nodup_iota

added theorem list.nodup_of_fn

added theorem list.nodup_range'

added theorem list.nodup_range

added theorem list.not_mem_range_self

added theorem list.nth_le_range

added theorem list.nth_range'

added theorem list.nth_range

added theorem list.of_fn_eq_pmap

added theorem list.pairwise_gt_iota

added theorem list.pairwise_lt_range'

added theorem list.pairwise_lt_range

added theorem list.prod_range_succ

added theorem list.range'_append

added theorem list.range'_concat

added theorem list.range'_eq_map_range

added theorem list.range'_sublist_right

added theorem list.range'_subset_right

added theorem list.range_concat

added theorem list.range_core_range'

added theorem list.range_eq_range'

added theorem list.range_sublist

added theorem list.range_subset

added theorem list.range_succ_eq_map

added theorem list.reverse_range'

Created src/data/list/rotate.lean

added theorem list.length_rotate'

added theorem list.length_rotate

added theorem list.mem_rotate

added theorem list.prod_rotate_eq_one_of_prod_eq_one

added theorem list.rotate'_cons_succ

added theorem list.rotate'_eq_take_append_drop

added theorem list.rotate'_length

added theorem list.rotate'_length_mul

added theorem list.rotate'_mod

added theorem list.rotate'_nil

added theorem list.rotate'_rotate'

added theorem list.rotate'_zero

added theorem list.rotate_cons_succ

added theorem list.rotate_eq_rotate'

added theorem list.rotate_eq_take_append_drop

added theorem list.rotate_length

added theorem list.rotate_length_mul

added theorem list.rotate_mod

added theorem list.rotate_nil

added theorem list.rotate_rotate

added theorem list.rotate_zero

Created src/data/list/sections.lean

added theorem list.mem_sections

added theorem list.mem_sections_length

added theorem list.rel_sections

Modified src/data/list/sigma.lean

Created src/data/list/tfae.lean

added theorem list.tfae.out

added def list.tfae

added theorem list.tfae_cons_cons

added theorem list.tfae_cons_of_mem

added theorem list.tfae_nil

added theorem list.tfae_of_cycle

added theorem list.tfae_of_forall

added theorem list.tfae_singleton

Created src/data/list/zip.lean

added theorem list.length_revzip

added theorem list.length_zip

added theorem list.mem_zip

added theorem list.reverse_revzip

added theorem list.revzip_map_fst

added theorem list.revzip_map_snd

added theorem list.revzip_swap

added theorem list.unzip_cons

added theorem list.unzip_eq_map

added theorem list.unzip_left

added theorem list.unzip_nil

added theorem list.unzip_revzip

added theorem list.unzip_right

added theorem list.unzip_swap

added theorem list.unzip_zip

added theorem list.unzip_zip_left

added theorem list.unzip_zip_right

added theorem list.zip_append

added theorem list.zip_cons_cons

added theorem list.zip_map'

added theorem list.zip_map

added theorem list.zip_map_left

added theorem list.zip_map_right

added theorem list.zip_nil_left

added theorem list.zip_nil_right

added theorem list.zip_swap

added theorem list.zip_unzip

Modified src/data/multiset.lean

Modified src/data/nat/modeq.lean

Modified src/data/vector2.lean

Modified src/group_theory/sylow.lean

Modified src/tactic/omega/coeffs.lean

Modified src/tactic/tfae.lean