Vector insertion helpers.

These are generic vector/list bridge operations used by determinant permutation enumerations and column-tuple constructions.

def Hex.Matrix.insertAt {α : Type u} {n : Nat} (x : α) (v : Vector α n) (i : Fin (n + 1)) : Vector α (n + 1)

Insert an element into a vector at a given position.

Equations

• Hex.Matrix.insertAt x v i = Vector.mk (v.toList.insertIdx (↑i) x).toArray ⋯

theorem Hex.Matrix.insertAt_get_self {α : Type u} {n : Nat} (x : α) (v : Vector α n) (i : Fin (n + 1)) : (insertAt x v i)[i] = x

Reading insertAt x v i at the insertion position i returns the inserted element x.

theorem Hex.Matrix.insertAt_last_get_castSucc {α : Type u} {n : Nat} (x : α) (v : Vector α n) (i : Fin n) : (insertAt x v (Fin.last n))[i.castSucc] = v[i]

After inserting x at Fin.last n, reading the result at i.castSucc returns the original entry v[i].

theorem Hex.Matrix.list_insertIdx_length {α : Type u} (xs : List α) (x : α) : xs.insertIdx xs.length x = xs ++ [x]

Inserting an element at index xs.length is the same as appending it.

theorem Hex.Matrix.vector_toList_map {α β : Type u} {n : Nat} (v : Vector α n) (f : α → β) : (Vector.map f v).toList = List.map f v.toList

Vector.map commutes with Vector.toList.

theorem Hex.Matrix.insertAt_last_toList {α : Type u} {n : Nat} (x : α) (v : Vector α n) : (insertAt x v (Fin.last n)).toList = v.toList ++ [x]

insertAt x v (Fin.last n) appends x to the end of v.toList.

theorem Hex.Matrix.insertAt_toList {α : Type u} {n : Nat} (x : α) (v : Vector α n) (i : Fin (n + 1)) : (insertAt x v i).toList = v.toList.insertIdx (↑i) x

insertAt x v i corresponds to List.insertIdx at position i on the underlying list.