chore(data/vector): rename vector2 (#8697)

This file was named this way to avoid clashing with `data/vector.lean` in core.
This renames it to `data/vector/basic.lean` which avoids the problem.

There was never a `vector2` definition, this was only ever a filename.

scripts/nolints.txt

@@ -364,7 +364,7 @@ apply_nolint wseq.mem doc_blame
 apply_nolint wseq.tail.aux doc_blame
 apply_nolint wseq.think_congr unused_arguments
 
--- data/vector2.lean
+-- data/vector/basic.lean
 apply_nolint vector.insert_nth doc_blame
 apply_nolint vector.m_of_fn doc_blame
 apply_nolint vector.mmap doc_blame
@@ -1056,4 +1056,4 @@ apply_nolint uniform_space.completion.map₂ doc_blame
 
 -- topology/uniform_space/uniform_embedding.lean
 apply_nolint uniform_embedding doc_blame
-apply_nolint uniform_inducing doc_blame
+apply_nolint uniform_inducing doc_blame

src/data/array/lemmas.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 import control.traversable.equiv
-import data.vector2
+import data.vector.basic
 
 universes u v w
 

src/data/bitvec/core.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Sebastian Ullrich
 -/
 
-import data.vector2
+import data.vector.basic
 import data.nat.basic
 
 /-!

src/data/sym/basic.lean

@@ -5,7 +5,7 @@ Authors: Kyle Miller
 -/
 
 import data.multiset.basic
-import data.vector2
+import data.vector.basic
 
 /-!
 # Symmetric powers

src/data/vector2.lean → src/data/vector/basic.lean

@@ -8,7 +8,7 @@ import data.list.nodup
 import data.list.of_fn
 import control.applicative
 /-!
-# Additional theorems about the `vector` type
+# Additional theorems and definitions about the `vector` type
 
 This file introduces the infix notation `::ᵥ` for `vector.cons`.
 -/