# mathlib3documentation

data.fin.vec_notation

# Matrix and vector notation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

## Implementation notes #

The simp lemmas require that one of the arguments is of the form vec_cons _ _. 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.

## Notations #

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

## Examples #

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

def matrix.vec_empty {α : Type u} :
fin 0 α

![] is the vector with no entries.

Equations
def matrix.vec_cons {α : Type u} {n : } (h : α) (t : fin n α) :
fin n.succ α

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

The inverse functions are vec_head and vec_tail. The notation ![a, b, ...] expands to vec_cons a (vec_cons b ...).

Equations
• = t
def matrix.vec_head {α : Type u} {n : } (v : fin n.succ α) :
α

vec_head v gives the first entry of the vector v

Equations
• = v 0
def matrix.vec_tail {α : Type u} {n : } (v : fin n.succ α) :
fin n α

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

Equations
@[protected, instance]
def pi_fin.has_repr {α : Type u} {n : } [has_repr α] :

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

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

Equations
theorem matrix.empty_eq {α : Type u} (v : fin 0 α) :
@[simp]
theorem matrix.head_fin_const {α : Type u} {n : } (a : α) :
matrix.vec_head (λ (i : fin (n + 1)), a) = a
@[simp]
theorem matrix.cons_val_zero {α : Type u} {m : } (x : α) (u : fin m α) :
0 = x
theorem matrix.cons_val_zero' {α : Type u} {m : } (h : 0 < m.succ) (x : α) (u : fin m α) :
0, h⟩ = x
@[simp]
theorem matrix.cons_val_succ {α : Type u} {m : } (x : α) (u : fin m α) (i : fin m) :
i.succ = u i
@[simp]
theorem matrix.cons_val_succ' {α : Type u} {m i : } (h : i.succ < m.succ) (x : α) (u : fin m α) :
i.succ, h⟩ = u i, _⟩
@[simp]
theorem matrix.head_cons {α : Type u} {m : } (x : α) (u : fin m α) :
= x
@[simp]
theorem matrix.tail_cons {α : Type u} {m : } (x : α) (u : fin m α) :
= u
@[simp]
theorem matrix.empty_val' {α : Type u} {n' : Type u_1} (j : n') :
(λ (i : fin 0), j) = matrix.vec_empty
@[simp]
theorem matrix.cons_head_tail {α : Type u} {m : } (u : fin m.succ α) :
@[simp]
theorem matrix.range_cons {α : Type u} {n : } (x : α) (u : fin n α) :
set.range u) = {x}
@[simp]
theorem matrix.range_empty {α : Type u} (u : fin 0 α) :
@[simp]
theorem matrix.range_cons_empty {α : Type u} (x : α) (u : fin 0 α) :
set.range u) = {x}
@[simp]
theorem matrix.range_cons_cons_empty {α : Type u} (x y : α) (u : fin 0 α) :
set.range u)) = {x, y}
@[simp]
theorem matrix.vec_cons_const {α : Type u} {n : } (a : α) :
(λ (k : fin n), a) = λ (_x : fin n.succ), a
theorem matrix.vec_single_eq_const {α : Type u} (a : α) :
![a] = λ (_x : fin 1), a
@[simp]
theorem matrix.cons_val_one {α : Type u} {m : } (x : α) (u : fin m.succ α) :
1 =

![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.

@[simp]
theorem matrix.cons_val_fin_one {α : Type u} (x : α) (u : fin 0 α) (i : fin 1) :
i = x
theorem matrix.cons_fin_one {α : Type u} (x : α) (u : fin 0 α) :
= λ (_x : fin 1), x
@[protected, instance]
meta def pi_fin.reflect {α : Type u} [reflected (Type u) α] [has_reflect α] {n : } :
meta def pi_fin.to_pexpr {n : } :

Convert a vector of pexprs to the pexpr constructing that vector.

### Numeral (bit0 and bit1) indices #

The following definitions and simp lemmas are to allow any numeral-indexed element of a vector given with matrix notation to be extracted by simp (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.vec_append {m n : } {α : Type u_1} {o : } (ho : o = m + n) (u : fin m α) (v : fin n α) :
fin o α

vec_append 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 vec_append ho u v 0 is valid. fin.append u v 0 is not valid in this case because there is no has_zero (fin (m + n)) instance.

Equations
theorem matrix.vec_append_eq_ite {m n : } {α : Type u_1} {o : } (ho : o = m + n) (u : fin m α) (v : fin n α) :
v = λ (i : fin o), dite (i < m) (λ (h : i < m), u i, h⟩) (λ (h : ¬i < m), v i - m, _⟩)
@[simp]
theorem matrix.vec_append_apply_zero {m n : } {α : Type u_1} {o : } (ho : o + 1 = m + 1 + n) (u : fin (m + 1) α) (v : fin n α) :
v 0 = u 0
@[simp]
theorem matrix.empty_vec_append {α : Type u} {n : } (v : fin n α) :
@[simp]
theorem matrix.cons_vec_append {α : Type u} {m n o : } (ho : o + 1 = m + 1 + n) (x : α) (u : fin m α) (v : fin n α) :
u) v = v)
def matrix.vec_alt0 {α : Type u} {m n : } (hm : m = n + n) (v : fin m α) (k : fin n) :
α

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

Equations
def matrix.vec_alt1 {α : Type u} {m n : } (hm : m = n + n) (v : fin m α) (k : fin n) :
α

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

Equations
theorem matrix.vec_alt0_vec_append {α : Type u} {n : } (v : fin n α) :
=
theorem matrix.vec_alt1_vec_append {α : Type u} {n : } (v : fin (n + 1) α) :
=
@[simp]
theorem matrix.vec_head_vec_alt0 {α : Type u} {m n : } (hm : m + 2 = n + 1 + (n + 1)) (v : fin (m + 2) α) :
= v 0
@[simp]
theorem matrix.vec_head_vec_alt1 {α : Type u} {m n : } (hm : m + 2 = n + 1 + (n + 1)) (v : fin (m + 2) α) :
= v 1
@[simp]
theorem matrix.cons_vec_bit0_eq_alt0 {α : Type u} {n : } (x : α) (u : fin n α) (i : fin (n + 1)) :
(bit0 i) = u)) i
@[simp]
theorem matrix.cons_vec_bit1_eq_alt1 {α : Type u} {n : } (x : α) (u : fin n α) (i : fin (n + 1)) :
(bit1 i) = u)) i
@[simp]
theorem matrix.cons_vec_alt0 {α : Type u} {m n : } (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : fin m α) :
u)) = u)
@[simp]
theorem matrix.empty_vec_alt0 (α : Type u_1) {h : 0 = 0 + 0} :
@[simp]
theorem matrix.cons_vec_alt1 {α : Type u} {m n : } (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : fin m α) :
u)) = u)
@[simp]
theorem matrix.empty_vec_alt1 (α : Type u_1) {h : 0 = 0 + 0} :
@[simp]
theorem matrix.smul_empty {α : Type u} {M : Type u_4} [ α] (x : M) (v : fin 0 α) :
@[simp]
theorem matrix.smul_cons {α : Type u} {n : } {M : Type u_4} [ α] (x : M) (y : α) (v : fin n α) :
x = matrix.vec_cons (x y) (x v)
@[simp]
theorem matrix.empty_add_empty {α : Type u} [has_add α] (v w : fin 0 α) :
@[simp]
theorem matrix.cons_add {α : Type u} {n : } [has_add α] (x : α) (v : fin n α) (w : fin n.succ α) :
+ w = (v +
@[simp]
theorem matrix.add_cons {α : Type u} {n : } [has_add α] (v : fin n.succ α) (y : α) (w : fin n α) :
v + = + w)
@[simp]
theorem matrix.cons_add_cons {α : Type u} {n : } [has_add α] (x : α) (v : fin n α) (y : α) (w : fin n α) :
+ = matrix.vec_cons (x + y) (v + w)
@[simp]
theorem matrix.head_add {α : Type u} {n : } [has_add α] (a b : fin n.succ α) :
@[simp]
theorem matrix.tail_add {α : Type u} {n : } [has_add α] (a b : fin n.succ α) :
@[simp]
theorem matrix.empty_sub_empty {α : Type u} [has_sub α] (v w : fin 0 α) :
@[simp]
theorem matrix.cons_sub {α : Type u} {n : } [has_sub α] (x : α) (v : fin n α) (w : fin n.succ α) :
- w = (v -
@[simp]
theorem matrix.sub_cons {α : Type u} {n : } [has_sub α] (v : fin n.succ α) (y : α) (w : fin n α) :
v - = - w)
@[simp]
theorem matrix.cons_sub_cons {α : Type u} {n : } [has_sub α] (x : α) (v : fin n α) (y : α) (w : fin n α) :
- = matrix.vec_cons (x - y) (v - w)
@[simp]
theorem matrix.head_sub {α : Type u} {n : } [has_sub α] (a b : fin n.succ α) :
@[simp]
theorem matrix.tail_sub {α : Type u} {n : } [has_sub α] (a b : fin n.succ α) :
@[simp]
theorem matrix.zero_empty {α : Type u} [has_zero α] :
@[simp]
theorem matrix.cons_zero_zero {α : Type u} {n : } [has_zero α] :
= 0
@[simp]
theorem matrix.head_zero {α : Type u} {n : } [has_zero α] :
@[simp]
theorem matrix.tail_zero {α : Type u} {n : } [has_zero α] :
@[simp]
theorem matrix.cons_eq_zero_iff {α : Type u} {n : } [has_zero α] {v : fin n α} {x : α} :
= 0 x = 0 v = 0
theorem matrix.cons_nonzero_iff {α : Type u} {n : } [has_zero α] {v : fin n α} {x : α} :
0 x 0 v 0
@[simp]
theorem matrix.neg_empty {α : Type u} [has_neg α] (v : fin 0 α) :
@[simp]
theorem matrix.neg_cons {α : Type u} {n : } [has_neg α] (x : α) (v : fin n α) :
- = (-v)
@[simp]
theorem matrix.head_neg {α : Type u} {n : } [has_neg α] (a : fin n.succ α) :
@[simp]
theorem matrix.tail_neg {α : Type u} {n : } [has_neg α] (a : fin n.succ α) :