# Documentation

## Mathlib.Data.Vector.Defs

The type Vector represents lists with fixed length.

def Mathlib.Vector (α : Type u) (n : ) :

Vector α n is the type of lists of length n with elements of type α.

Equations
• = { l : List α // l.length = n }
Instances For
instance Mathlib.Vector.instDecidableEq {α : Type u} {n : } [] :
Equations
@[match_pattern]
def Mathlib.Vector.nil {α : Type u} :

The empty vector with elements of type α

Equations
• Mathlib.Vector.nil = [],
Instances For
@[match_pattern]
def Mathlib.Vector.cons {α : Type u} {n : } :
αMathlib.Vector α n.succ

If a : α and l : Vector α n, then cons a l, is the vector of length n + 1 whose first element is a and with l as the rest of the list.

Equations
• = match x✝, x with | a, v, h => a :: v,
Instances For
@[reducible]
def Mathlib.Vector.length {α : Type u} {n : } :

The length of a vector.

Equations
• x.length = n
Instances For
def Mathlib.Vector.head {α : Type u} {n : } :
Mathlib.Vector α n.succα

The first element of a vector with length at least 1.

Equations
• x.head = match x with | a :: tail, property => a
Instances For
theorem Mathlib.Vector.head_cons {α : Type u} {n : } (a : α) (v : ) :

The head of a vector obtained by prepending is the element prepended.

def Mathlib.Vector.tail {α : Type u} {n : } :
Mathlib.Vector α (n - 1)

The tail of a vector, with an empty vector having empty tail.

Equations
• x.tail = match x with | [], h => [], | head :: v, h => v,
Instances For
theorem Mathlib.Vector.tail_cons {α : Type u} {n : } (a : α) (v : ) :
().tail = v

The tail of a vector obtained by prepending is the vector prepended. to

@[simp]
theorem Mathlib.Vector.cons_head_tail {α : Type u} {n : } (v : Mathlib.Vector α n.succ) :

Prepending the head of a vector to its tail gives the vector.

def Mathlib.Vector.toList {α : Type u} {n : } (v : ) :
List α

The list obtained from a vector.

Equations
• v.toList = v
Instances For
def Mathlib.Vector.get {α : Type u} {n : } (l : ) (i : Fin n) :
α

nth element of a vector, indexed by a Fin type.

Equations
Instances For
def Mathlib.Vector.append {α : Type u} {n : } {m : } :
Mathlib.Vector α (n + m)

Appending a vector to another.

Equations
• x✝.append x = match x✝, x with | l₁, h₁, l₂, h₂ => l₁ ++ l₂,
Instances For
def Mathlib.Vector.elim {α : Type u_1} {C : {n : } → Sort u} (H : (l : List α) → C l, ) {n : } (v : ) :
C v

Elimination rule for Vector.

Equations
• = match x with | l, h => match n, h with | .(l.length), => H l
Instances For
def Mathlib.Vector.map {α : Type u} {β : Type v} {n : } (f : αβ) :

Map a vector under a function.

Equations
• = match x with | l, h => List.map f l,
Instances For
@[simp]
theorem Mathlib.Vector.map_nil {α : Type u} {β : Type v} (f : αβ) :
Mathlib.Vector.map f Mathlib.Vector.nil = Mathlib.Vector.nil

A nil vector maps to a nil vector.

@[simp]
theorem Mathlib.Vector.map_cons {α : Type u} {β : Type v} {n : } (f : αβ) (a : α) (v : ) :

map is natural with respect to cons.

def Mathlib.Vector.map₂ {α : Type u} {β : Type v} {φ : Type w} {n : } (f : αβφ) :

Mapping two vectors under a curried function of two variables.

Equations
• = match x✝, x with | x, property, y, property_1 => List.zipWith f x y,
Instances For
def Mathlib.Vector.replicate {α : Type u} (n : ) (a : α) :

Vector obtained by repeating an element.

Equations
• = ⟨,
Instances For
def Mathlib.Vector.drop {α : Type u} {n : } (i : ) :
Mathlib.Vector α (n - i)

Drop i elements from a vector of length n; we can have i > n.

Equations
• = match x with | l, p => ⟨,
Instances For
def Mathlib.Vector.take {α : Type u} {n : } (i : ) :
Mathlib.Vector α (min i n)

Take i elements from a vector of length n; we can have i > n.

Equations
• = match x with | l, p => ⟨,
Instances For
def Mathlib.Vector.eraseIdx {α : Type u} {n : } (i : Fin n) :
Mathlib.Vector α (n - 1)

Remove the element at position i from a vector of length n.

Equations
• = match x with | l, p => l.eraseIdx i,
Instances For
@[deprecated Mathlib.Vector.eraseIdx]
def Mathlib.Vector.removeNth {α : Type u} {n : } (i : Fin n) :
Mathlib.Vector α (n - 1)

Alias of Mathlib.Vector.eraseIdx.

Remove the element at position i from a vector of length n.

Equations
Instances For
def Mathlib.Vector.ofFn {α : Type u} {n : } :
(Fin nα)

Vector of length n from a function on Fin n.

Equations
Instances For
def Mathlib.Vector.congr {α : Type u} {n : } {m : } (h : n = m) :

Create a vector from another with a provably equal length.

Equations
• = match x with | x, p => x,
Instances For
def Mathlib.Vector.mapAccumr {α : Type u} {β : Type v} {n : } {σ : Type} (f : ασσ × β) :
σσ ×

Runs a function over a vector returning the intermediate results and a final result.

Equations
• = match x✝, x with | x, px, c => let res := ; (res.fst, res.snd, )
Instances For
def Mathlib.Vector.mapAccumr₂ {n : } {α : Type} {β : Type} {σ : Type} {φ : Type} (f : αβσσ × φ) :
σσ ×

Runs a function over a pair of vectors returning the intermediate results and a final result.

Equations
Instances For

### Shift Primitives #

def Mathlib.Vector.shiftLeftFill {α : Type u} {n : } (v : ) (i : ) (fill : α) :

shiftLeftFill v i is the vector obtained by left-shifting v i times and padding with the fill argument. If v.length < i then this will return replicate n fill.

Equations
Instances For
def Mathlib.Vector.shiftRightFill {α : Type u} {n : } (v : ) (i : ) (fill : α) :

shiftRightFill v i is the vector obtained by right-shifting v i times and padding with the fill argument. If v.length < i then this will return replicate n fill.

Equations
Instances For

### Basic Theorems #

theorem Mathlib.Vector.eq {α : Type u} {n : } (a1 : ) (a2 : ) :
a1.toList = a2.toLista1 = a2

Vector is determined by the underlying list.

theorem Mathlib.Vector.eq_nil {α : Type u} (v : ) :
v = Mathlib.Vector.nil

A vector of length 0 is a nil vector.

@[simp]
theorem Mathlib.Vector.toList_mk {α : Type u} {n : } (v : List α) (P : v.length = n) :

Vector of length from a list v with witness that v has length n maps to v under toList.

@[simp]
theorem Mathlib.Vector.toList_nil {α : Type u} :
Mathlib.Vector.nil.toList = []

A nil vector maps to a nil list.

@[simp]
theorem Mathlib.Vector.toList_length {α : Type u} {n : } (v : ) :
v.toList.length = n

The length of the list to which a vector of length n maps is n.

@[simp]
theorem Mathlib.Vector.toList_cons {α : Type u} {n : } (a : α) (v : ) :
().toList = a :: v.toList

toList of cons of a vector and an element is the cons of the list obtained by toList and the element

@[simp]
theorem Mathlib.Vector.toList_append {α : Type u} {n : } {m : } (v : ) (w : ) :
(v.append w).toList = v.toList ++ w.toList

Appending of vectors corresponds under toList to appending of lists.

@[simp]
theorem Mathlib.Vector.toList_drop {α : Type u} {n : } {m : } (v : ) :
().toList = List.drop n v.toList

drop of vectors corresponds under toList to drop of lists.

@[simp]
theorem Mathlib.Vector.toList_take {α : Type u} {n : } {m : } (v : ) :
().toList = List.take n v.toList

take of vectors corresponds under toList to take of lists.

instance Mathlib.Vector.instGetElemNatLt {α : Type u} {n : } :
GetElem () α fun (x : ) (i : ) => i < n
Equations
• Mathlib.Vector.instGetElemNatLt = { getElem := fun (x : ) (i : ) (h : i < n) => x.get i, h }