Theorems · Theorem · combinatorics

List.Vector.toList_singleton

∀ {α : Type u_1} (v : List.Vector α 1), v.toList = [v.head]

The list that makes up a Vector made up of a single element, retrieved via toList, is equal to the list of that single element.

Defined in

Mathlib.Data.Vector.Basic

Cited by

2 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext