mathlib documentation

data.matrix.notation

Matrix and vector notation #

This file includes simp lemmas for applying operations in data.matrix.basic to values built out of the matrix notation ![a, b] = vec_cons a (vec_cons b vec_empty) defined in data.fin.vec_notation.

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 #

We reuse notation ![a, b] for vec_cons a (vec_cons b vec_empty). It is a localized notation in the matrix locale.

Examples #

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

@[protected, instance]
def matrix.has_repr {α : Type u} {n m : } [has_repr α] :
has_repr (matrix (fin m) (fin n) α)

Use ![...] notation for displaying a fin-indexed matrix, for example:

#eval ![![1, 2], ![3, 4]] + ![![3, 4], ![5, 6]] -- ![![4, 6], ![8, 10]]
Equations
@[simp]
theorem matrix.cons_val' {α : Type u} {m : } {n' : Type u_2} (v : n' → α) (B : matrix (fin m) n' α) (i : fin m.succ) (j : n') :
matrix.vec_cons v B i j = matrix.vec_cons (v j) (λ (i : fin m), B i j) i
@[simp]
theorem matrix.head_val' {α : Type u} {m : } {n' : Type u_2} (B : matrix (fin m.succ) n' α) (j : n') :
matrix.vec_head (λ (i : fin m.succ), B i j) = matrix.vec_head B j
@[simp]
theorem matrix.tail_val' {α : Type u} {m : } {n' : Type u_2} (B : matrix (fin m.succ) n' α) (j : n') :
matrix.vec_tail (λ (i : fin m.succ), B i j) = λ (i : fin m), matrix.vec_tail B i j
@[simp]
theorem matrix.dot_product_empty {α : Type u} [add_comm_monoid α] [has_mul α] (v w : fin 0 → α) :
@[simp]
theorem matrix.cons_dot_product {α : Type u} {n : } [add_comm_monoid α] [has_mul α] (x : α) (v : fin n → α) (w : fin n.succ → α) :
@[simp]
theorem matrix.dot_product_cons {α : Type u} {n : } [add_comm_monoid α] [has_mul α] (v : fin n.succ → α) (x : α) (w : fin n → α) :
@[simp]
theorem matrix.cons_dot_product_cons {α : Type u} {n : } [add_comm_monoid α] [has_mul α] (x : α) (v : fin n → α) (y : α) (w : fin n → α) :
@[simp]
theorem matrix.col_empty {α : Type u} (v : fin 0 → α) :
@[simp]
theorem matrix.col_cons {α : Type u} {m : } (x : α) (u : fin m → α) :
@[simp]
theorem matrix.row_empty {α : Type u} :
@[simp]
theorem matrix.row_cons {α : Type u} {m : } (x : α) (u : fin m → α) :
@[simp]
theorem matrix.transpose_empty_rows {α : Type u} {m' : Type u_1} (A : matrix m' (fin 0) α) :
@[simp]
theorem matrix.transpose_empty_cols {α : Type u} {m' : Type u_1} :
@[simp]
theorem matrix.cons_transpose {α : Type u} {m : } {n' : Type u_2} (v : n' → α) (A : matrix (fin m) n' α) :
@[simp]
theorem matrix.head_transpose {α : Type u} {n : } {m' : Type u_1} (A : matrix m' (fin n.succ) α) :
@[simp]
theorem matrix.tail_transpose {α : Type u} {n : } {m' : Type u_1} (A : matrix m' (fin n.succ) α) :
@[simp]
theorem matrix.empty_mul {α : Type u} {n' : Type u_2} {o' : Type u_3} [semiring α] [fintype n'] (A : matrix (fin 0) n' α) (B : matrix n' o' α) :
@[simp]
theorem matrix.empty_mul_empty {α : Type u} {m' : Type u_1} {o' : Type u_3} [semiring α] (A : matrix m' (fin 0) α) (B : matrix (fin 0) o' α) :
A.mul B = 0
@[simp]
theorem matrix.mul_empty {α : Type u} {m' : Type u_1} {n' : Type u_2} [semiring α] [fintype n'] (A : matrix m' n' α) (B : matrix n' (fin 0) α) :
A.mul B = λ (_x : m'), matrix.vec_empty
theorem matrix.mul_val_succ {α : Type u} {m : } {n' : Type u_2} {o' : Type u_3} [semiring α] [fintype n'] (A : matrix (fin m.succ) n' α) (B : matrix n' o' α) (i : fin m) (j : o') :
A.mul B i.succ j = matrix.mul (matrix.vec_tail A) B i j
@[simp]
theorem matrix.cons_mul {α : Type u} {m : } {n' : Type u_2} {o' : Type u_3} [semiring α] [fintype n'] (v : n' → α) (A : matrix (fin m) n' α) (B : matrix n' o' α) :
@[simp]
theorem matrix.empty_vec_mul {α : Type u} {o' : Type u_3} [semiring α] (v : fin 0 → α) (B : matrix (fin 0) o' α) :
@[simp]
theorem matrix.vec_mul_empty {α : Type u} {n' : Type u_2} [semiring α] [fintype n'] (v : n' → α) (B : matrix n' (fin 0) α) :
@[simp]
theorem matrix.cons_vec_mul {α : Type u} {n : } {o' : Type u_3} [semiring α] (x : α) (v : fin n → α) (B : matrix (fin n.succ) o' α) :
@[simp]
theorem matrix.vec_mul_cons {α : Type u} {n : } {o' : Type u_3} [semiring α] (v : fin n.succ → α) (w : o' → α) (B : matrix (fin n) o' α) :
@[simp]
theorem matrix.empty_mul_vec {α : Type u} {n' : Type u_2} [semiring α] [fintype n'] (A : matrix (fin 0) n' α) (v : n' → α) :
@[simp]
theorem matrix.mul_vec_empty {α : Type u} {m' : Type u_1} [semiring α] (A : matrix m' (fin 0) α) (v : fin 0 → α) :
A.mul_vec v = 0
@[simp]
theorem matrix.cons_mul_vec {α : Type u} {m : } {n' : Type u_2} [semiring α] [fintype n'] (v : n' → α) (A : fin mn' → α) (w : n' → α) :
@[simp]
theorem matrix.mul_vec_cons {n : } {m' : Type u_1} {α : Type u_2} [comm_semiring α] (A : m' → fin n.succ → α) (x : α) (v : fin n → α) :
@[simp]
theorem matrix.empty_vec_mul_vec {α : Type u} {n' : Type u_2} [semiring α] (v : fin 0 → α) (w : n' → α) :
@[simp]
theorem matrix.vec_mul_vec_empty {α : Type u} {m' : Type u_1} [semiring α] (v : m' → α) (w : fin 0 → α) :
@[simp]
theorem matrix.cons_vec_mul_vec {α : Type u} {m : } {n' : Type u_2} [semiring α] (x : α) (v : fin m → α) (w : n' → α) :
@[simp]
theorem matrix.vec_mul_vec_cons {α : Type u} {n : } {m' : Type u_1} [semiring α] (v : m' → α) (x : α) (w : fin n → α) :
@[simp]
theorem matrix.smul_mat_empty {α : Type u} [semiring α] {m' : Type u_1} (x : α) (A : fin 0m' → α) :
@[simp]
theorem matrix.smul_mat_cons {α : Type u} {m : } {n' : Type u_2} [semiring α] (x : α) (v : n' → α) (A : matrix (fin m) n' α) :
@[simp]
theorem matrix.minor_empty {α : Type u} {m' : Type u_1} {n' : Type u_2} {o' : Type u_3} (A : matrix m' n' α) (row : fin 0 → m') (col : o' → n') :
@[simp]
theorem matrix.minor_cons_row {α : Type u} {m : } {m' : Type u_1} {n' : Type u_2} {o' : Type u_3} (A : matrix m' n' α) (i : m') (row : fin m → m') (col : o' → n') :
A.minor (matrix.vec_cons i row) col = matrix.vec_cons (λ (j : o'), A i (col j)) (A.minor row col)
theorem matrix.one_fin_two {α : Type u} [has_zero α] [has_one α] :
1 = ![![1, 0], ![0, 1]]
theorem matrix.one_fin_three {α : Type u} [has_zero α] [has_one α] :
1 = ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]]
theorem matrix.mul_fin_two {α : Type u} [add_comm_monoid α] [has_mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
matrix.mul ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] ![![b₁₁, b₁₂], ![b₂₁, b₂₂]] = ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
theorem matrix.mul_fin_three {α : Type u} [add_comm_monoid α] [has_mul α] (a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α) :
matrix.mul ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]] = ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃], ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃], ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
theorem matrix.vec2_eq {α : Type u} {a₀ a₁ b₀ b₁ : α} (h₀ : a₀ = b₀) (h₁ : a₁ = b₁) :
![a₀, a₁] = ![b₀, b₁]
theorem matrix.vec3_eq {α : Type u} {a₀ a₁ a₂ b₀ b₁ b₂ : α} (h₀ : a₀ = b₀) (h₁ : a₁ = b₁) (h₂ : a₂ = b₂) :
![a₀, a₁, a₂] = ![b₀, b₁, b₂]
theorem matrix.vec2_add {α : Type u} [has_add α] (a₀ a₁ b₀ b₁ : α) :
![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]
theorem matrix.vec3_add {α : Type u} [has_add α] (a₀ a₁ a₂ b₀ b₁ b₂ : α) :
![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]
theorem matrix.smul_vec2 {α : Type u} {R : Type u_1} [has_scalar R α] (x : R) (a₀ a₁ : α) :
x ![a₀, a₁] = ![x a₀, x a₁]
theorem matrix.smul_vec3 {α : Type u} {R : Type u_1} [has_scalar R α] (x : R) (a₀ a₁ a₂ : α) :
x ![a₀, a₁, a₂] = ![x a₀, x a₁, x a₂]
theorem matrix.vec2_dot_product' {α : Type u} [add_comm_monoid α] [has_mul α] {a₀ a₁ b₀ b₁ : α} :
matrix.dot_product ![a₀, a₁] ![b₀, b₁] = a₀ * b₀ + a₁ * b₁
@[simp]
theorem matrix.vec2_dot_product {α : Type u} [add_comm_monoid α] [has_mul α] (v w : fin 2 → α) :
matrix.dot_product v w = v 0 * w 0 + v 1 * w 1
theorem matrix.vec3_dot_product' {α : Type u} [add_comm_monoid α] [has_mul α] {a₀ a₁ a₂ b₀ b₁ b₂ : α} :
matrix.dot_product ![a₀, a₁, a₂] ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂
@[simp]
theorem matrix.vec3_dot_product {α : Type u} [add_comm_monoid α] [has_mul α] (v w : fin 3 → α) :
matrix.dot_product v w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2