Commit 2024-12-15 09:21 07a54609

View on Github →

chore: rename Mathlib.Vector to List.Vector (#19930) Per @digama0's suggestion on zulip.

Estimated changes

Modified .github/PULL_REQUEST_TEMPLATE.md

Modified Mathlib/Computability/Halting.lean

modified def Nat.Partrec'.Vec

modified theorem Nat.Partrec'.comp₁

modified theorem Nat.Partrec'.of_eq

modified theorem Nat.Partrec'.of_prim

modified theorem Nat.Partrec'.rfindOpt

modified inductive Nat.Partrec'

Modified Mathlib/Computability/Partrec.lean

modified theorem Computable.vector_cons

modified theorem Computable.vector_get

modified theorem Computable.vector_head

modified theorem Computable.vector_length

modified theorem Computable.vector_ofFn'

modified theorem Computable.vector_tail

modified theorem Computable.vector_toList

Modified Mathlib/Computability/Primrec.lean

modified def Nat.Primrec'.Vec

modified theorem Nat.Primrec'.of_eq

modified inductive Nat.Primrec'

modified theorem Primrec.vector_cons

modified theorem Primrec.vector_get'

modified theorem Primrec.vector_get

modified theorem Primrec.vector_head

modified theorem Primrec.vector_length

modified theorem Primrec.vector_ofFn'

modified theorem Primrec.vector_tail

modified theorem Primrec.vector_toList

modified theorem Primrec.vector_toList_iff

Modified Mathlib/Computability/TMToPartrec.lean

modified theorem Turing.ToPartrec.Code.exists_code.comp

modified theorem Turing.ToPartrec.Code.exists_code

Modified Mathlib/Computability/TuringMachine.lean

modified def Turing.TM1to1.readAux

Modified Mathlib/Data/Finite/Vector.lean

Modified Mathlib/Data/Fintype/BigOperators.lean

Modified Mathlib/Data/Fintype/Fin.lean

modified theorem Fin.card_filter_univ_eq_vector_get_eq_count

Modified Mathlib/Data/Fintype/Vector.lean

Modified Mathlib/Data/Num/Bitwise.lean

modified def SNum.bits

Modified Mathlib/Data/Set/Finite/List.lean

modified theorem List.finite_length_eq

Modified Mathlib/Data/Sym/Basic.lean

modified theorem Sym.cons_of_coe_eq

modified def Sym.ofVector

modified theorem Sym.ofVector_cons

modified theorem Sym.ofVector_nil

modified theorem Sym.sound

Modified Mathlib/Data/Sym/Sym2.lean

Modified Mathlib/Data/Vector/Basic.lean

added theorem List.Vector.Vector.append_nil

added theorem List.Vector.Vector.get_append_cons_succ

added theorem List.Vector.Vector.get_append_cons_zero

added theorem List.Vector.Vector.get_map₂

added theorem List.Vector.Vector.mapAccumr_cons

added theorem List.Vector.Vector.mapAccumr₂_cons

added theorem List.Vector.Vector.replicate_succ

added def List.Vector.casesOn

added def List.Vector.casesOn₂

added def List.Vector.casesOn₃

added theorem List.Vector.cons_val

added theorem List.Vector.empty_toList_eq_ff

added theorem List.Vector.eq_cons_iff

added theorem List.Vector.eraseIdx_insertIdx'

added theorem List.Vector.eraseIdx_insertIdx

added theorem List.Vector.eraseIdx_val

added theorem List.Vector.exists_eq_cons

added theorem List.Vector.ext

added theorem List.Vector.getElem_map

added theorem List.Vector.getElem_pmap

added theorem List.Vector.get_cons_nil

added theorem List.Vector.get_cons_succ

added theorem List.Vector.get_cons_zero

added theorem List.Vector.get_eq_get

added theorem List.Vector.get_map

added theorem List.Vector.get_ofFn

added theorem List.Vector.get_replicate

added theorem List.Vector.get_set_eq_if

added theorem List.Vector.get_set_of_ne

added theorem List.Vector.get_set_same

added theorem List.Vector.get_tail

added theorem List.Vector.get_tail_succ

added theorem List.Vector.get_zero

added theorem List.Vector.head?_toList

added theorem List.Vector.head_map

added theorem List.Vector.head_ofFn

added theorem List.Vector.head_pmap

added def List.Vector.inductionOn

added theorem List.Vector.inductionOn_cons

added theorem List.Vector.inductionOn_nil

added def List.Vector.inductionOn₂

added def List.Vector.inductionOn₃

added def List.Vector.insertIdx

added theorem List.Vector.insertIdx_comm

added theorem List.Vector.insertIdx_val

added def List.Vector.last

added theorem List.Vector.last_def

added theorem List.Vector.length_val

added def List.Vector.mOfFn

added theorem List.Vector.mOfFn_pure

added theorem List.Vector.map_id

added theorem List.Vector.map₂_cons

added theorem List.Vector.map₂_nil

added theorem List.Vector.mk_toList

added def List.Vector.mmap

added theorem List.Vector.mmap_cons

added theorem List.Vector.mmap_nil

added theorem List.Vector.ne_cons_iff

added theorem List.Vector.nodup_iff_injective_get

added theorem List.Vector.not_empty_toList

added theorem List.Vector.ofFn_get

added theorem List.Vector.pmap_cons'

added theorem List.Vector.pmap_cons

added theorem List.Vector.prod_set'

added theorem List.Vector.prod_set

added def List.Vector.reverse

added theorem List.Vector.reverse_get_zero

added theorem List.Vector.reverse_reverse

added def List.Vector.scanl

added theorem List.Vector.scanl_cons

added theorem List.Vector.scanl_get

added theorem List.Vector.scanl_head

added theorem List.Vector.scanl_nil

added theorem List.Vector.scanl_singleton

added theorem List.Vector.scanl_val

added def List.Vector.set

added theorem List.Vector.singleton_tail

added theorem List.Vector.tail_map

added theorem List.Vector.tail_nil

added theorem List.Vector.tail_ofFn

added theorem List.Vector.tail_pmap

added theorem List.Vector.tail_val

added def List.Vector.toArray

added theorem List.Vector.toList_empty

added theorem List.Vector.toList_injective

added theorem List.Vector.toList_map

added theorem List.Vector.toList_ofFn

added theorem List.Vector.toList_pmap

added theorem List.Vector.toList_reverse

added theorem List.Vector.toList_scanl

added theorem List.Vector.toList_set

added theorem List.Vector.toList_singleton

deleted theorem Mathlib.Vector.append_nil

deleted def Mathlib.Vector.casesOn

deleted def Mathlib.Vector.casesOn₂

deleted def Mathlib.Vector.casesOn₃

deleted theorem Mathlib.Vector.cons_val

deleted theorem Mathlib.Vector.empty_toList_eq_ff

deleted theorem Mathlib.Vector.eq_cons_iff

deleted theorem Mathlib.Vector.eraseIdx_insertIdx'

deleted theorem Mathlib.Vector.eraseIdx_insertIdx

deleted theorem Mathlib.Vector.eraseIdx_val

deleted theorem Mathlib.Vector.exists_eq_cons

deleted theorem Mathlib.Vector.ext

deleted theorem Mathlib.Vector.getElem_map

deleted theorem Mathlib.Vector.getElem_pmap

deleted theorem Mathlib.Vector.get_append_cons_succ

deleted theorem Mathlib.Vector.get_append_cons_zero

deleted theorem Mathlib.Vector.get_cons_nil

deleted theorem Mathlib.Vector.get_cons_succ

deleted theorem Mathlib.Vector.get_cons_zero

deleted theorem Mathlib.Vector.get_eq_get

deleted theorem Mathlib.Vector.get_map

deleted theorem Mathlib.Vector.get_map₂

deleted theorem Mathlib.Vector.get_ofFn

deleted theorem Mathlib.Vector.get_replicate

deleted theorem Mathlib.Vector.get_set_eq_if

deleted theorem Mathlib.Vector.get_set_of_ne

deleted theorem Mathlib.Vector.get_set_same

deleted theorem Mathlib.Vector.get_tail

deleted theorem Mathlib.Vector.get_tail_succ

deleted theorem Mathlib.Vector.get_zero

deleted theorem Mathlib.Vector.head?_toList

deleted theorem Mathlib.Vector.head_map

deleted theorem Mathlib.Vector.head_ofFn

deleted theorem Mathlib.Vector.head_pmap

deleted def Mathlib.Vector.inductionOn

deleted theorem Mathlib.Vector.inductionOn_cons

deleted theorem Mathlib.Vector.inductionOn_nil

deleted def Mathlib.Vector.inductionOn₂

deleted def Mathlib.Vector.inductionOn₃

deleted def Mathlib.Vector.insertIdx

deleted theorem Mathlib.Vector.insertIdx_comm

deleted theorem Mathlib.Vector.insertIdx_val

deleted def Mathlib.Vector.last

deleted theorem Mathlib.Vector.last_def

deleted theorem Mathlib.Vector.length_val

deleted def Mathlib.Vector.mOfFn

deleted theorem Mathlib.Vector.mOfFn_pure

deleted theorem Mathlib.Vector.mapAccumr_cons

deleted theorem Mathlib.Vector.mapAccumr₂_cons

deleted theorem Mathlib.Vector.map_id

deleted theorem Mathlib.Vector.map₂_cons

deleted theorem Mathlib.Vector.map₂_nil

deleted theorem Mathlib.Vector.mk_toList

deleted def Mathlib.Vector.mmap

deleted theorem Mathlib.Vector.mmap_cons

deleted theorem Mathlib.Vector.mmap_nil

deleted theorem Mathlib.Vector.ne_cons_iff

deleted theorem Mathlib.Vector.nodup_iff_injective_get

deleted theorem Mathlib.Vector.not_empty_toList

deleted theorem Mathlib.Vector.ofFn_get

deleted theorem Mathlib.Vector.pmap_cons'

deleted theorem Mathlib.Vector.pmap_cons

deleted theorem Mathlib.Vector.prod_set'

deleted theorem Mathlib.Vector.prod_set

deleted theorem Mathlib.Vector.replicate_succ

deleted def Mathlib.Vector.reverse

deleted theorem Mathlib.Vector.reverse_get_zero

deleted theorem Mathlib.Vector.reverse_reverse

deleted def Mathlib.Vector.scanl

deleted theorem Mathlib.Vector.scanl_cons

deleted theorem Mathlib.Vector.scanl_get

deleted theorem Mathlib.Vector.scanl_head

deleted theorem Mathlib.Vector.scanl_nil

deleted theorem Mathlib.Vector.scanl_singleton

deleted theorem Mathlib.Vector.scanl_val

deleted def Mathlib.Vector.set

deleted theorem Mathlib.Vector.singleton_tail

deleted theorem Mathlib.Vector.tail_map

deleted theorem Mathlib.Vector.tail_nil

deleted theorem Mathlib.Vector.tail_ofFn

deleted theorem Mathlib.Vector.tail_pmap

deleted theorem Mathlib.Vector.tail_val

deleted def Mathlib.Vector.toArray

deleted theorem Mathlib.Vector.toList_empty

deleted theorem Mathlib.Vector.toList_injective

deleted theorem Mathlib.Vector.toList_map

deleted theorem Mathlib.Vector.toList_ofFn

deleted theorem Mathlib.Vector.toList_pmap

deleted theorem Mathlib.Vector.toList_reverse

deleted theorem Mathlib.Vector.toList_scanl

deleted theorem Mathlib.Vector.toList_set

deleted theorem Mathlib.Vector.toList_singleton

Modified Mathlib/Data/Vector/Defs.lean

added def List.Vector.append

added def List.Vector.cons

added theorem List.Vector.cons_head_tail

added def List.Vector.drop

added def List.Vector.elim

added def List.Vector.eraseIdx

added def List.Vector.get

added theorem List.Vector.getElem_def

added def List.Vector.head

added theorem List.Vector.head_cons

added def List.Vector.length

added def List.Vector.map

added def List.Vector.mapAccumr

added def List.Vector.mapAccumr₂

added theorem List.Vector.map_cons

added theorem List.Vector.map_nil

added def List.Vector.map₂

added def List.Vector.nil

added def List.Vector.ofFn

added def List.Vector.pmap

added theorem List.Vector.pmap_nil

added def List.Vector.replicate

added def List.Vector.shiftLeftFill

added def List.Vector.shiftRightFill

added def List.Vector.tail

added theorem List.Vector.tail_cons

added def List.Vector.take

added def List.Vector.toList

added theorem List.Vector.toList_append

added theorem List.Vector.toList_cons

added theorem List.Vector.toList_drop

added theorem List.Vector.toList_getElem

added theorem List.Vector.toList_length

added theorem List.Vector.toList_mk

added theorem List.Vector.toList_nil

added theorem List.Vector.toList_take

added def List.Vector

deleted def Mathlib.Vector.append

deleted def Mathlib.Vector.cons

deleted theorem Mathlib.Vector.cons_head_tail

deleted def Mathlib.Vector.drop

deleted def Mathlib.Vector.elim

deleted def Mathlib.Vector.eraseIdx

deleted def Mathlib.Vector.get

deleted theorem Mathlib.Vector.getElem_def

deleted def Mathlib.Vector.head

deleted theorem Mathlib.Vector.head_cons

deleted def Mathlib.Vector.length

deleted def Mathlib.Vector.map

deleted def Mathlib.Vector.mapAccumr

deleted def Mathlib.Vector.mapAccumr₂

deleted theorem Mathlib.Vector.map_cons

deleted theorem Mathlib.Vector.map_nil

deleted def Mathlib.Vector.map₂

deleted def Mathlib.Vector.nil

deleted def Mathlib.Vector.ofFn

deleted def Mathlib.Vector.pmap

deleted theorem Mathlib.Vector.pmap_nil

deleted def Mathlib.Vector.replicate

deleted def Mathlib.Vector.shiftLeftFill

deleted def Mathlib.Vector.shiftRightFill

deleted def Mathlib.Vector.tail

deleted theorem Mathlib.Vector.tail_cons

deleted def Mathlib.Vector.take

deleted def Mathlib.Vector.toList

deleted theorem Mathlib.Vector.toList_append

deleted theorem Mathlib.Vector.toList_cons

deleted theorem Mathlib.Vector.toList_drop

deleted theorem Mathlib.Vector.toList_getElem

deleted theorem Mathlib.Vector.toList_length

deleted theorem Mathlib.Vector.toList_mk

deleted theorem Mathlib.Vector.toList_nil

deleted theorem Mathlib.Vector.toList_take

deleted def Mathlib.Vector

Modified Mathlib/Data/Vector/MapLemmas.lean

added theorem List.Vector.mapAccumr_bisim

added theorem List.Vector.mapAccumr_bisim_tail

added theorem List.Vector.mapAccumr_eq_map

added theorem List.Vector.mapAccumr_eq_map_of_constant_state

added theorem List.Vector.mapAccumr_eq_map_of_unused_state

added theorem List.Vector.mapAccumr_map

added theorem List.Vector.mapAccumr_mapAccumr

added theorem List.Vector.mapAccumr_mapAccumr₂

added theorem List.Vector.mapAccumr_redundant_pair

added theorem List.Vector.mapAccumr₂_bisim

added theorem List.Vector.mapAccumr₂_bisim_tail

added theorem List.Vector.mapAccumr₂_comm

added theorem List.Vector.mapAccumr₂_eq_map₂

added theorem List.Vector.mapAccumr₂_eq_map₂_of_constant_state

added theorem List.Vector.mapAccumr₂_eq_map₂_of_unused_state

added theorem List.Vector.mapAccumr₂_flip

added theorem List.Vector.mapAccumr₂_mapAccumr_left

added theorem List.Vector.mapAccumr₂_mapAccumr_right

added theorem List.Vector.mapAccumr₂_mapAccumr₂_left_left

added theorem List.Vector.mapAccumr₂_mapAccumr₂_left_right

added theorem List.Vector.mapAccumr₂_mapAccumr₂_right_left

added theorem List.Vector.mapAccumr₂_mapAccumr₂_right_right

added theorem List.Vector.mapAccumr₂_redundant_pair

added theorem List.Vector.mapAccumr₂_unused_input_left

added theorem List.Vector.mapAccumr₂_unused_input_right

added theorem List.Vector.map_map

added theorem List.Vector.map_mapAccumr

added theorem List.Vector.map_map₂

added theorem List.Vector.map_pmap

added theorem List.Vector.map₂_comm

added theorem List.Vector.map₂_flip

added theorem List.Vector.map₂_map_left

added theorem List.Vector.map₂_map_right

added theorem List.Vector.pmap_map

deleted theorem Mathlib.Vector.mapAccumr_bisim

deleted theorem Mathlib.Vector.mapAccumr_bisim_tail

deleted theorem Mathlib.Vector.mapAccumr_eq_map

deleted theorem Mathlib.Vector.mapAccumr_eq_map_of_constant_state

deleted theorem Mathlib.Vector.mapAccumr_eq_map_of_unused_state

deleted theorem Mathlib.Vector.mapAccumr_map

deleted theorem Mathlib.Vector.mapAccumr_mapAccumr

deleted theorem Mathlib.Vector.mapAccumr_mapAccumr₂

deleted theorem Mathlib.Vector.mapAccumr_redundant_pair

deleted theorem Mathlib.Vector.mapAccumr₂_bisim

deleted theorem Mathlib.Vector.mapAccumr₂_bisim_tail

deleted theorem Mathlib.Vector.mapAccumr₂_comm

deleted theorem Mathlib.Vector.mapAccumr₂_eq_map₂

deleted theorem Mathlib.Vector.mapAccumr₂_eq_map₂_of_constant_state

deleted theorem Mathlib.Vector.mapAccumr₂_eq_map₂_of_unused_state

deleted theorem Mathlib.Vector.mapAccumr₂_flip

deleted theorem Mathlib.Vector.mapAccumr₂_mapAccumr_left

deleted theorem Mathlib.Vector.mapAccumr₂_mapAccumr_right

deleted theorem Mathlib.Vector.mapAccumr₂_mapAccumr₂_left_left

deleted theorem Mathlib.Vector.mapAccumr₂_mapAccumr₂_left_right

deleted theorem Mathlib.Vector.mapAccumr₂_mapAccumr₂_right_left

deleted theorem Mathlib.Vector.mapAccumr₂_mapAccumr₂_right_right

deleted theorem Mathlib.Vector.mapAccumr₂_redundant_pair

deleted theorem Mathlib.Vector.mapAccumr₂_unused_input_left

deleted theorem Mathlib.Vector.mapAccumr₂_unused_input_right

deleted theorem Mathlib.Vector.map_map

deleted theorem Mathlib.Vector.map_mapAccumr

deleted theorem Mathlib.Vector.map_map₂

deleted theorem Mathlib.Vector.map_pmap

deleted theorem Mathlib.Vector.map₂_comm

deleted theorem Mathlib.Vector.map₂_flip

deleted theorem Mathlib.Vector.map₂_map_left

deleted theorem Mathlib.Vector.map₂_map_right

deleted theorem Mathlib.Vector.pmap_map

Modified Mathlib/Data/Vector/Mem.lean

added theorem List.Vector.get_mem

added theorem List.Vector.head_mem

added theorem List.Vector.mem_cons_iff

added theorem List.Vector.mem_cons_of_mem

added theorem List.Vector.mem_cons_self

added theorem List.Vector.mem_iff_get

added theorem List.Vector.mem_map_iff

added theorem List.Vector.mem_map_succ_iff

added theorem List.Vector.mem_of_mem_tail

added theorem List.Vector.mem_succ_iff

added theorem List.Vector.not_mem_map_zero

added theorem List.Vector.not_mem_nil

added theorem List.Vector.not_mem_zero

deleted theorem Mathlib.Vector.get_mem

deleted theorem Mathlib.Vector.head_mem

deleted theorem Mathlib.Vector.mem_cons_iff

deleted theorem Mathlib.Vector.mem_cons_of_mem

deleted theorem Mathlib.Vector.mem_cons_self

deleted theorem Mathlib.Vector.mem_iff_get

deleted theorem Mathlib.Vector.mem_map_iff

deleted theorem Mathlib.Vector.mem_map_succ_iff

deleted theorem Mathlib.Vector.mem_of_mem_tail

deleted theorem Mathlib.Vector.mem_succ_iff

deleted theorem Mathlib.Vector.not_mem_map_zero

deleted theorem Mathlib.Vector.not_mem_nil

deleted theorem Mathlib.Vector.not_mem_zero

Modified Mathlib/Data/Vector/Snoc.lean

added theorem List.Vector.mapAccumr_nil

added theorem List.Vector.mapAccumr_snoc

added theorem List.Vector.mapAccumr₂_nil

added theorem List.Vector.mapAccumr₂_snoc

added theorem List.Vector.map_snoc

added theorem List.Vector.map₂_snoc

added theorem List.Vector.replicate_succ_to_snoc

added def List.Vector.revCasesOn

added def List.Vector.revInductionOn

added def List.Vector.revInductionOn₂

added theorem List.Vector.reverse_cons

added theorem List.Vector.reverse_snoc

added def List.Vector.snoc

added theorem List.Vector.snoc_cons

added theorem List.Vector.snoc_nil

deleted theorem Mathlib.Vector.mapAccumr_nil

deleted theorem Mathlib.Vector.mapAccumr_snoc

deleted theorem Mathlib.Vector.mapAccumr₂_nil

deleted theorem Mathlib.Vector.mapAccumr₂_snoc

deleted theorem Mathlib.Vector.map_snoc

deleted theorem Mathlib.Vector.map₂_snoc

deleted theorem Mathlib.Vector.replicate_succ_to_snoc

deleted def Mathlib.Vector.revCasesOn

deleted def Mathlib.Vector.revInductionOn

deleted def Mathlib.Vector.revInductionOn₂

deleted theorem Mathlib.Vector.reverse_cons

deleted theorem Mathlib.Vector.reverse_snoc

deleted def Mathlib.Vector.snoc

deleted theorem Mathlib.Vector.snoc_cons

deleted theorem Mathlib.Vector.snoc_nil

Modified Mathlib/Data/Vector/Zip.lean

added theorem List.Vector.prod_mul_prod_eq_prod_zipWith

added def List.Vector.zipWith

added theorem List.Vector.zipWith_get

added theorem List.Vector.zipWith_tail

added theorem List.Vector.zipWith_toList

deleted theorem Mathlib.Vector.prod_mul_prod_eq_prod_zipWith

deleted def Mathlib.Vector.zipWith

deleted theorem Mathlib.Vector.zipWith_get

deleted theorem Mathlib.Vector.zipWith_tail

deleted theorem Mathlib.Vector.zipWith_toList

Modified Mathlib/GroupTheory/Perm/Cycle/Type.lean

modified def Equiv.Perm.VectorsProdEqOne.equivVector

modified theorem Equiv.Perm.VectorsProdEqOne.mem_iff

modified def Equiv.Perm.VectorsProdEqOne.vectorEquiv

modified def Equiv.Perm.vectorsProdEqOne

Modified Mathlib/Logic/Equiv/List.lean

Modified Mathlib/Logic/Small/List.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

modified theorem Cardinal.mk_vector

Modified Mathlib/Topology/List.lean

modified theorem Vector.continuous_insertIdx

modified theorem Vector.tendsto_cons

Modified MathlibTest/NthRewrite.lean

Modified MathlibTest/cc.lean

Modified scripts/nolints_prime_decls.txt