Theorems · Theorem · combinatorics

List.Vector.eq_cons_iff

∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n.succ) (v' : List.Vector α n),
  v = a ::ᵥ v' ↔ v.head = a ∧ v.tail = v'

Defined in

Mathlib.Data.Vector.Basic

Cited by

2 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms