toList_drop — Mathlib

English

Drop on vector corresponds under toList to drop on lists: toList (drop n v) = List.drop n (toList v).

Русский

Drop векторности соответствует drop в списках: toList (drop n v) = List.drop n (toList v).

LaTeX

$$@[simp]\\ntheorem toList_drop {n m : \\mathbb{N}} (v : Vector α m) : toList (drop n v) = List.drop n (toList v)$$

Lean4

/-- `drop` of vectors corresponds under `toList` to `drop` of lists. -/
@[simp]
theorem toList_drop {n m : ℕ} (v : Vector α m) : toList (drop n v) = List.drop n (toList v) :=
  by
  cases v
  rfl

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