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.
