Matrix and vector notation

This file defines notation for vectors and matrices. Given a b c d : α, the notation allows us to write ![a, b, c, d] : Fin 4 → α. Nesting vectors gives coefficients of a matrix, so ![![a, b], ![c, d]] : Fin 2 → Fin 2 → α. In later files we introduce !![a, b; c, d] as notation for Matrix.of ![![a, b], ![c, d]].

Main definitions

• vecEmpty is the empty vector (or 0 by n matrix) ![]
• vecCons prepends an entry to a vector, so ![a, b] is vecCons a (vecCons b vecEmpty)

Implementation notes

The simp lemmas require that one of the arguments is of the form vecCons _ _. This ensures simp works with entries only when (some) entries are already given. In other words, this notation will only appear in the output of simp if it already appears in the input.

Notation

The main new notation is ![a, b], which gets expanded to vecCons a (vecCons b vecEmpty).

Examples

Examples of usage can be found in the MathlibTest/matrix.lean file.

def Matrix.vecEmpty {α : Type u} : Fin 0 → α

![] is the vector with no entries.

Equations

• ![] = Fin.elim0

def Matrix.vecCons {α : Type u} {n : ℕ} (h : α) (t : Fin n → α) : Fin n.succ → α

vecCons h t prepends an entry h to a vector t.

The inverse functions are vecHead and vecTail. The notation ![a, b, ...] expands to vecCons a (vecCons b ...).

Equations

• Matrix.vecCons h t = Fin.cons h t

def Matrix.vecNotation : Lean.ParserDescr

![...] notation is used to construct a vector Fin n → α using Matrix.vecEmpty and Matrix.vecCons.

For instance, ![a, b, c] : Fin 3 is syntax for vecCons a (vecCons b (vecCons c vecEmpty)).

Note that this should not be used as syntax for Matrix as it generates a term with the wrong type. The !![a, b; c, d] syntax (provided by Matrix.matrixNotation) should be used instead.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.vecConsUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the ![x, y, ...] notation.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.vecEmptyUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the ![] notation.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.vecHead {α : Type u} {n : ℕ} (v : Fin n.succ → α) : α

vecHead v gives the first entry of the vector v

Equations

• Matrix.vecHead v = v 0

def Matrix.vecTail {α : Type u} {n : ℕ} (v : Fin n.succ → α) : Fin n → α

vecTail v gives a vector consisting of all entries of v except the first

Equations

• Matrix.vecTail v = v ∘ Fin.succ

@[instance_reducible]

instance PiFin.hasRepr {α : Type u} {n : ℕ} [Repr α] : Repr (Fin n → α)

Use ![...] notation for displaying a vector Fin n → α, for example:

#eval ![1, 2] + ![3, 4] -- ![4, 6]

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.empty_eq {α : Type u} (v : Fin 0 → α) : v = ![]

@[simp]

theorem Matrix.head_fin_const {α : Type u} {n : ℕ} (a : α) : (vecHead fun (x : Fin (n + 1)) => a) = a

@[simp]

theorem Matrix.cons_val_zero {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) : vecCons x u 0 = x

theorem Matrix.cons_val_zero' {α : Type u} {m : ℕ} (h : 0 < m.succ) (x : α) (u : Fin m → α) : vecCons x u ⟨0, h⟩ = x

@[simp]

theorem Matrix.cons_val_succ {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) (i : Fin m) : vecCons x u i.succ = u i

@[simp]

theorem Matrix.cons_val_succ' {α : Type u} {m i : ℕ} (h : i.succ < m.succ) (x : α) (u : Fin m → α) : vecCons x u ⟨i.succ, h⟩ = u ⟨i, ⋯⟩

@[simp]

theorem Matrix.Fin.cons_vecEmpty {α : Type u_1} (x : α) : Fin.cons x ![] = ![x]

We don't want to always simplify Fin.cons to vecCons. But in cases that we are already mixing the declarations for dependent tuples and non-dependent tuples, we can simplify to the non-dependent tuples.

@[simp]

theorem Matrix.Fin.snoc_vecEmpty {α : Type u_1} (x : α) : Fin.snoc ![] x = ![x]

Simplify Fin.snoc to vecCons in this case.

@[simp]

theorem Matrix.Fin.cons_vecCons {n : ℕ} {α : Type u_1} (x y : α) (p : Fin n → α) : Fin.cons x (vecCons y p) = vecCons x (vecCons y p)

We don't want to always simplify Fin.cons to vecCons. But in cases that we are already mixing the declarations for dependent tuples and non-dependent tuples, we can simplify to the non-dependent tuples. This allows us to simplify Fin.cons 5 ![1, 3, 7] to ![5, 1, 3, 7].

@[simp]

theorem Matrix.Fin.snoc_vecCons {n : ℕ} {α : Type u_1} (x y : α) (p : Fin n → α) : Fin.snoc (vecCons y p) x = vecCons y (Fin.snoc p x)

We push Fin.snoc inside vecCons. This allows us to simplify e.g. Fin.snoc ![1, 3, 7] 5 to ![1, 3, 7, 5].

partial def Matrix.matchVecConsPrefix (n : Q(ℕ)) (e : Lean.Expr) : Lean.MetaM (List Lean.Expr × Q(ℕ) × Lean.Expr)

Parses a chain of Matrix.vecCons calls into elements, leaving everything else in the tail.

let ⟨xs, tailn, tail⟩ ← matchVecConsPrefix n e decomposes e : Fin n → _ in the form vecCons x₀ <| ... <| vecCons xₙ <| tail where tail : Fin tailn → _.

def Matrix.cons_val : Lean.Meta.Simp.DSimproc

A simproc that handles terms of the form Matrix.vecCons a f i where i is a numeric literal.

In practice, this is most effective at handling ![a, b, c] i-style terms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.head_cons {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) : vecHead (vecCons x u) = x

@[simp]

theorem Matrix.tail_cons {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) : vecTail (vecCons x u) = u

@[simp]

theorem Fin.tail_vecCons {α : Type u} {n : ℕ} (x : α) (t : Fin n → α) : tail (Matrix.vecCons x t) = t

theorem Matrix.empty_val' {α : Type u} {n' : Type u_1} (j : n') : (fun (i : Fin 0) => ![] i j) = ![]

@[simp]

theorem Matrix.cons_head_tail {α : Type u} {m : ℕ} (u : Fin m.succ → α) : vecCons (vecHead u) (vecTail u) = u

@[simp]

theorem Matrix.range_cons {α : Type u} {n : ℕ} (x : α) (u : Fin n → α) : Set.range (vecCons x u) = {x} ∪ Set.range u

@[simp]

theorem Matrix.range_empty {α : Type u} (u : Fin 0 → α) : Set.range u = ∅

theorem Matrix.range_cons_empty {α : Type u} (x : α) (u : Fin 0 → α) : Set.range (vecCons x u) = {x}

theorem Matrix.range_cons_cons_empty {α : Type u} (x y : α) (u : Fin 0 → α) : Set.range (vecCons x (vecCons y u)) = {x, y}

theorem Matrix.vecCons_const {α : Type u} {n : ℕ} (a : α) : (vecCons a fun (x : Fin n) => a) = fun (x : Fin n.succ) => a

theorem Matrix.vec_single_eq_const {α : Type u} (a : α) : ![a] = fun (x : Fin (Nat.succ 0)) => a

@[simp]

theorem Matrix.cons_val_one {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ → α) : vecCons x u 1 = u 0

![a, b, ...] 1 is equal to b.

The simplifier needs a special lemma for length ≥ 2, in addition to cons_val_succ, because 1 : Fin 1 = 0 : Fin 1.

theorem Matrix.cons_val_two {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ.succ → α) : vecCons x u 2 = vecHead (vecTail u)

theorem Matrix.cons_val_three {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ.succ.succ → α) : vecCons x u 3 = vecHead (vecTail (vecTail u))

theorem Matrix.cons_val_four {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ.succ.succ.succ → α) : vecCons x u 4 = vecHead (vecTail (vecTail (vecTail u)))

@[simp]

theorem Matrix.cons_val_fin_one {α : Type u} (x : α) (u : Fin 0 → α) (i : Fin 1) : vecCons x u i = x

theorem Matrix.cons_fin_one {α : Type u} (x : α) (u : Fin 0 → α) : vecCons x u = fun (x_1 : Fin (Nat.succ 0)) => x

@[simp]

theorem Matrix.vecCons_inj {α : Type u} {n : ℕ} {x y : α} {u v : Fin n → α} : vecCons x u = vecCons y v ↔ x = y ∧ u = v

def PiFin.mkLiteralQ {u : Lean.Level} {α : Q(Type u)} {n : ℕ} (elems : Fin n → Q(«$α»)) : Q(Fin «$n» → «$α»)

mkVecLiteralQ ![x, y, z] produces the term q(![$x, $y, $z]).

Equations

• PiFin.mkLiteralQ elems = PiFin.mkLiteralQ.loop✝ elems 0 q(![])

@[instance_reducible]

instance PiFin.toExpr {α : Type u} [Lean.ToLevel] [Lean.ToExpr α] (n : ℕ) : Lean.ToExpr (Fin n → α)

bit0 and bit1 indices

The following definitions and simp lemmas are used to allow numeral-indexed element of a vector given with matrix notation to be extracted by simp in Lean 3 (even when the numeral is larger than the number of elements in the vector, which is taken modulo that number of elements by virtue of the semantics of bit0 and bit1 and of addition on Fin n).

def Matrix.vecAppend {m n : ℕ} {α : Type u_1} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α) : Fin o → α

vecAppend ho u v appends two vectors of lengths m and n to produce one of length o = m + n. This is a variant of Fin.append with an additional ho argument, which provides control of definitional equality for the vector length.

This turns out to be helpful when providing simp lemmas to reduce ![a, b, c] n, and also means that vecAppend ho u v 0 is valid. Fin.append u v 0 is not valid in this case because there is no Zero (Fin (m + n)) instance.

Equations

• Matrix.vecAppend ho u v = Fin.append u v ∘ Fin.cast ho

theorem Matrix.vecAppend_eq_ite {m n : ℕ} {α : Type u_1} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α) : vecAppend ho u v = fun (i : Fin o) => if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

@[simp]

theorem Matrix.vecAppend_apply_zero {m n : ℕ} {α : Type u_1} {o : ℕ} (ho : o + 1 = m + 1 + n) (u : Fin (m + 1) → α) (v : Fin n → α) : vecAppend ho u v 0 = u 0

@[simp]

theorem Matrix.empty_vecAppend {α : Type u} {n : ℕ} (v : Fin n → α) : vecAppend ⋯ ![] v = v

@[simp]

theorem Matrix.vecAppend_empty {α : Type u} {n : ℕ} (v : Fin n → α) : vecAppend ⋯ v ![] = v

@[simp]

theorem Matrix.cons_vecAppend {α : Type u} {m n o : ℕ} (ho : o + 1 = m + 1 + n) (x : α) (u : Fin m → α) (v : Fin n → α) : vecAppend ho (vecCons x u) v = vecCons x (vecAppend ⋯ u v)

def Matrix.vecAlt0 {α : Type u} {m n : ℕ} (hm : m = n + n) (v : Fin m → α) (k : Fin n) : α

vecAlt0 v gives a vector with half the length of v, with only alternate elements (even-numbered).

Equations

• Matrix.vecAlt0 hm v k = v ⟨↑k + ↑k, ⋯⟩

def Matrix.vecAlt1 {α : Type u} {m n : ℕ} (hm : m = n + n) (v : Fin m → α) (k : Fin n) : α

vecAlt1 v gives a vector with half the length of v, with only alternate elements (odd-numbered).

Equations

• Matrix.vecAlt1 hm v k = v ⟨↑k + ↑k + 1, ⋯⟩

theorem Matrix.vecAlt0_vecAppend {α : Type u} {n : ℕ} (v : Fin n → α) : vecAlt0 ⋯ (vecAppend ⋯ v v) = v ∘ fun (n_1 : Fin n) => n_1 + n_1

theorem Matrix.vecAlt1_vecAppend {α : Type u} {n : ℕ} (v : Fin (n + 1) → α) : vecAlt1 ⋯ (vecAppend ⋯ v v) = v ∘ fun (n_1 : Fin (n + 1)) => n_1 + n_1 + 1

@[simp]

theorem Matrix.vecHead_vecAlt0 {α : Type u} {m n : ℕ} (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) : vecHead (vecAlt0 hm v) = v 0

@[simp]

theorem Matrix.vecHead_vecAlt1 {α : Type u} {m n : ℕ} (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) : vecHead (vecAlt1 hm v) = v 1

theorem Matrix.cons_vec_bit0_eq_alt0 {α : Type u} {n : ℕ} (x : α) (u : Fin n → α) (i : Fin (n + 1)) : vecCons x u (i + i) = vecAlt0 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

theorem Matrix.cons_vec_bit1_eq_alt1 {α : Type u} {n : ℕ} (x : α) (u : Fin n → α) (i : Fin (n + 1)) : vecCons x u (i + i + 1) = vecAlt1 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

@[simp]

theorem Matrix.cons_vecAlt0 {α : Type u} {m n : ℕ} (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) : vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 ⋯ u)

@[simp]

theorem Matrix.empty_vecAlt0 (α : Type u_1) {h : 0 = 0 + 0} : vecAlt0 h ![] = ![]

@[simp]

theorem Matrix.cons_vecAlt1 {α : Type u} {m n : ℕ} (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) : vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 ⋯ u)

@[simp]

theorem Matrix.empty_vecAlt1 (α : Type u_1) {h : 0 = 0 + 0} : vecAlt1 h ![] = ![]

theorem Matrix.const_fin1_eq {α : Type u} (x : α) : (fun (x_1 : Fin 1) => x) = ![x]

Interaction between cons and Equiv.swap

@[simp]

theorem Matrix.cons_cons_comp_swap_zero_one {α : Type u} {n : ℕ} (a b : α) (x : Fin n → α) : vecCons a (vecCons b x) ∘ ⇑(Equiv.swap 0 1) = vecCons b (vecCons a x)

theorem Matrix.cons_swap {α : Type u} {n : ℕ} (a : α) (x : Fin n → α) (i j : Fin n) : vecCons a (x ∘ ⇑(Equiv.swap i j)) = vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)

@[simp]

theorem Matrix.injective_pair_iff_ne {α : Type u} {x y : α} : Function.Injective ![x, y] ↔ x ≠ y

@[deprecated Matrix.injective_pair_iff_ne (since := "2026-09-04")]

theorem injective_pair_iff_ne {α : Type u} {x y : α} : Function.Injective ![x, y] ↔ x ≠ y

Alias of Matrix.injective_pair_iff_ne.