toList_length — Mathlib

English

The length of the list corresponding to a vector is its length: (toList v).length = n.

Русский

Длина списка, соответствующего вектору, равна его длине: (toList v).length = n.

LaTeX

$$@[simp]\\ntheorem toList_length (v : Vector α n) : (toList v).length = n$$

Lean4

/-- The length of the list to which a vector of length `n` maps is `n`. -/
@[simp]
theorem toList_length (v : Vector α n) : (toList v).length = n :=
  v.2

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