get — Mathlib

English

The ith element of a vector is defined by indexing into the underlying list with an adjusted index.

Русский

i-й элемент вектора определяется обращением к списку с адаптированным индексом.

LaTeX

$$$\\mathrm{get}(l, i) := l.1.\\mathrm{get}\\lvert i.cast\\, l.2.symm\\rvert$$$

Lean4

/-- nth element of a vector, indexed by a `Fin` type. -/
def get (l : Vector α n) (i : Fin n) : α :=
  l.1.get <| i.cast l.2.symm

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