vecTail — Mathlib

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

Похожие утверждения