English
Given h: n = m, there is a map congr that sends a vector of length n to length m by transporting the length along the equality.
Русский
Сопоставление векторов по равенству длин: если n = m, то вектор длины n можно рассматривать как вектор длины m через отображение congr.
LaTeX
$$$\\text{congr} : (h:\\, n=m) \\to (\\text{Vector }\\alpha n \\to \\text{Vector }\\alpha m),\\quad \\text{congr}(h)(\\langle x,p\\rangle)=\\langle x, h\\, p\\rangle$$$
Lean4
/-- Remove the element at position `i` from a vector of length `n`. -/
def eraseIdx (i : Fin n) : Vector α n → Vector α (n - 1)
| ⟨l, p⟩ => ⟨List.eraseIdx l i.1, by rw [l.length_eraseIdx_of_lt] <;> rw [p]; exact i.2⟩
