refactor: cleanup `Vector` API #9404

	on:
	push:
	branches-ignore:
	# ignore tmp branches used by bors
	- 'staging.tmp*'
	- 'trying.tmp*'
	- 'staging*.tmp'
	pull_request:

	name: ci

	jobs:
	build:
	name: Build
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4

	- id: lean-action
	name: build, test, and lint batteries
	uses: leanprover/lean-action@v1
	with:
	build-args: '--wfail'

	- name: Check that all files are imported
	run: lake env lean scripts/check_imports.lean

	- name: Check for forbidden character ↦
	if: always()
	run: \|
	if grep -r -n --include=\*.lean -e '↦' . ; then
	echo "Error: Found forbidden character ↦"
	exit 1
	fi

	- name: Check for 'namespace Mathlib'
	if: always()
	run: \|
	if grep -r -n --include=\*.lean -e 'namespace Mathlib' . ; then
	echo "Error: Found 'namespace Mathlib'"
	exit 1
	fi

	- name: Check for long lines
	if: always()
	run: \|
	! (find Batteries -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; \| grep -v -E 'https?://')

	- name: Check for trailing whitespace
	if: always()
	run: \|
	scripts/lintWhitespace.sh

	- name: Don't 'import Lean', use precise imports
	if: always()
	run: \|
	! (find . -name "*.lean" ! -path "./BatteriesTest/import_lean.lean" -type f -print0 \| xargs -0 grep -E -n '^import Lean$')

Provide feedback