English
The last element of a vector of length n+1 is obtained by getting the element at Fin.last n.
Русский
Последний элемент вектора длины n+1 равен элементу с индексом Fin.last n.
LaTeX
$$$\\forall {\\alpha} {n} (v:\\mathrm{Vector}\\ \\alpha\\ (n+1)),\\; v.last = v.get(\\mathrm{Fin.last}\\ n)$$$
Lean4
/-- The last element of a `Vector`, given that the vector is at least one element. -/
def last (v : Vector α (n + 1)) : α :=
v.get (Fin.last n)