English
vecTail v yields the vector consisting of all entries of v except the first, i.e., vecTail v = v ∘ Fin.succ.
Русский
vecTail v дает вектор, состоящий из всех элементов v, кроме первого: vecTail v = v ∘ Fin.succ.
LaTeX
$$$\\operatorname{vecTail}(v) = v \\circ \\operatorname{Fin}.succ$$$
Lean4
/-- `vecTail v` gives a vector consisting of all entries of `v` except the first -/
def vecTail {n : ℕ} (v : Fin n.succ → α) : Fin n → α :=
v ∘ Fin.succ