English
Two vectors are equal iff all their corresponding coordinates are equal.
Русский
Два вектора равны тогда и только тогда, когда все их координаты совпадают.
LaTeX
$$$\\forall {v w : \\mathrm{Vector}(\\alpha,n)}\\, (\\forall m : \\mathrm{Fin}(n), \\mathrm{Vector}.get\\ v\\ m = \\mathrm{Vector}.get\\ w\\ m) \\Rightarrow v = w$$$
Lean4
/-- Two `v w : Vector α n` are equal iff they are equal at every single index. -/
@[ext]
theorem ext : ∀ {v w : Vector α n} (_ : ∀ m : Fin n, Vector.get v m = Vector.get w m), v = w
| ⟨v, hv⟩, ⟨w, hw⟩, h => Subtype.eq (List.ext_get (by rw [hv, hw]) fun m hm _ => h ⟨m, hv ▸ hm⟩)
