# Row and column matrices #

This file provides results about row and column matrices

## Main definitions #

• Matrix.row r : Matrix Unit n α: a matrix with a single row
• Matrix.col c : Matrix m Unit α: a matrix with a single column
• Matrix.updateRow M i r: update the ith row of M to r
• Matrix.updateCol M j c: update the jth column of M to c
def Matrix.col {m : Type u_2} {α : Type v} (ι : Type u_6) (w : mα) :
Matrix m ι α

Matrix.col ι u the matrix with all columns equal to the vector u.

To get a column matrix with exactly one column, Matrix.col (Fin 1) u is the canonical choice.

Equations
• = Matrix.of fun (x : m) (x_1 : ι) => w x
Instances For
@[simp]
theorem Matrix.col_apply {m : Type u_2} {α : Type v} {ι : Type u_6} (w : mα) (i : m) (j : ι) :
Matrix.col ι w i j = w i
def Matrix.row {n : Type u_3} {α : Type v} (ι : Type u_6) (v : nα) :
Matrix ι n α

Matrix.row ι u the matrix with all rows equal to the vector u.

To get a row matrix with exactly one row, Matrix.row (Fin 1) u is the canonical choice.

Equations
• = Matrix.of fun (x : ι) (y : n) => v y
Instances For
@[simp]
theorem Matrix.row_apply {n : Type u_3} {α : Type v} {ι : Type u_6} (v : nα) (i : ι) (j : n) :
Matrix.row ι v i j = v j
theorem Matrix.col_injective {m : Type u_2} {α : Type v} {ι : Type u_6} [] :
@[simp]
theorem Matrix.col_inj {m : Type u_2} {α : Type v} {ι : Type u_6} [] {v : mα} {w : mα} :
= v = w
@[simp]
theorem Matrix.col_zero {m : Type u_2} {α : Type v} {ι : Type u_6} [Zero α] :
= 0
@[simp]
theorem Matrix.col_eq_zero {m : Type u_2} {α : Type v} {ι : Type u_6} [Zero α] [] (v : mα) :
= 0 v = 0
@[simp]
theorem Matrix.col_add {m : Type u_2} {α : Type v} {ι : Type u_6} [Add α] (v : mα) (w : mα) :
Matrix.col ι (v + w) = +
@[simp]
theorem Matrix.col_smul {m : Type u_2} {R : Type u_5} {α : Type v} {ι : Type u_6} [SMul R α] (x : R) (v : mα) :
Matrix.col ι (x v) = x
theorem Matrix.row_injective {n : Type u_3} {α : Type v} {ι : Type u_6} [] :
@[simp]
theorem Matrix.row_inj {n : Type u_3} {α : Type v} {ι : Type u_6} [] {v : nα} {w : nα} :
= v = w
@[simp]
theorem Matrix.row_zero {n : Type u_3} {α : Type v} {ι : Type u_6} [Zero α] :
= 0
@[simp]
theorem Matrix.row_eq_zero {n : Type u_3} {α : Type v} {ι : Type u_6} [Zero α] [] (v : nα) :
= 0 v = 0
@[simp]
theorem Matrix.row_add {m : Type u_2} {α : Type v} {ι : Type u_6} [Add α] (v : mα) (w : mα) :
Matrix.row ι (v + w) = +
@[simp]
theorem Matrix.row_smul {m : Type u_2} {R : Type u_5} {α : Type v} {ι : Type u_6} [SMul R α] (x : R) (v : mα) :
Matrix.row ι (x v) = x
@[simp]
theorem Matrix.transpose_col {m : Type u_2} {α : Type v} {ι : Type u_6} (v : mα) :
().transpose =
@[simp]
theorem Matrix.transpose_row {m : Type u_2} {α : Type v} {ι : Type u_6} (v : mα) :
().transpose =
@[simp]
theorem Matrix.conjTranspose_col {m : Type u_2} {α : Type v} {ι : Type u_6} [Star α] (v : mα) :
().conjTranspose = Matrix.row ι (star v)
@[simp]
theorem Matrix.conjTranspose_row {m : Type u_2} {α : Type v} {ι : Type u_6} [Star α] (v : mα) :
().conjTranspose = Matrix.col ι (star v)
theorem Matrix.row_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [] (M : Matrix m n α) (v : mα) :
Matrix.row ι () = * M
theorem Matrix.col_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [] (M : Matrix m n α) (v : mα) :
Matrix.col ι () = ( * M).transpose
theorem Matrix.col_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [] (M : Matrix m n α) (v : nα) :
Matrix.col ι (M.mulVec v) = M *
theorem Matrix.row_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [] (M : Matrix m n α) (v : nα) :
Matrix.row ι (M.mulVec v) = (M * ).transpose
@[simp]
theorem Matrix.row_mul_col_apply {m : Type u_2} {α : Type v} {ι : Type u_6} [] [Mul α] [] (v : mα) (w : mα) (i : ι) (j : ι) :
( * ) i j =
@[simp]
theorem Matrix.diag_col_mul_row {n : Type u_3} {α : Type v} {ι : Type u_6} [Mul α] [] [] (a : nα) (b : nα) :
( * ).diag = a * b
theorem Matrix.vecMulVec_eq {m : Type u_2} {n : Type u_3} {α : Type v} (ι : Type u_6) [Mul α] [] [] (w : mα) (v : nα) :
= *

### Updating rows and columns #

def Matrix.updateRow {m : Type u_2} {n : Type u_3} {α : Type v} [] (M : Matrix m n α) (i : m) (b : nα) :
Matrix m n α

Update, i.e. replace the ith row of matrix A with the values in b.

Equations
• M.updateRow i b = Matrix.of ()
Instances For
def Matrix.updateColumn {m : Type u_2} {n : Type u_3} {α : Type v} [] (M : Matrix m n α) (j : n) (b : mα) :
Matrix m n α

Update, i.e. replace the jth column of matrix A with the values in b.

Equations
Instances For
@[simp]
theorem Matrix.updateRow_self {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : nα} [] :
M.updateRow i b i = b
@[simp]
theorem Matrix.updateColumn_self {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : mα} [] :
M.updateColumn j c i j = c i
@[simp]
theorem Matrix.updateRow_ne {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : nα} [] {i' : m} (i_ne : i' i) :
M.updateRow i b i' = M i'
@[simp]
theorem Matrix.updateColumn_ne {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : mα} [] {j' : n} (j_ne : j' j) :
M.updateColumn j c i j' = M i j'
theorem Matrix.updateRow_apply {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {b : nα} [] {i' : m} :
M.updateRow i b i' j = if i' = i then b j else M i' j
theorem Matrix.updateColumn_apply {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : mα} [] {j' : n} :
M.updateColumn j c i j' = if j' = j then c i else M i j'
@[simp]
theorem Matrix.updateColumn_subsingleton {m : Type u_2} {n : Type u_3} {R : Type u_5} [] (A : Matrix m n R) (i : n) (b : mR) :
A.updateColumn i b = (Matrix.col (Fin 1) b).submatrix id ()
@[simp]
theorem Matrix.updateRow_subsingleton {m : Type u_2} {n : Type u_3} {R : Type u_5} [] (A : Matrix m n R) (i : m) (b : nR) :
A.updateRow i b = (Matrix.row (Fin 1) b).submatrix () id
theorem Matrix.map_updateRow {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {i : m} {b : nα} [] (f : αβ) :
(M.updateRow i b).map f = (M.map f).updateRow i (f b)
theorem Matrix.map_updateColumn {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {j : n} {c : mα} [] (f : αβ) :
(M.updateColumn j c).map f = (M.map f).updateColumn j (f c)
theorem Matrix.updateRow_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {j : n} {c : mα} [] :
M.transpose.updateRow j c = (M.updateColumn j c).transpose
theorem Matrix.updateColumn_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : nα} [] :
M.transpose.updateColumn i b = (M.updateRow i b).transpose
theorem Matrix.updateRow_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {j : n} {c : mα} [] [Star α] :
M.conjTranspose.updateRow j (star c) = (M.updateColumn j c).conjTranspose
theorem Matrix.updateColumn_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : nα} [] [Star α] :
M.conjTranspose.updateColumn i (star b) = (M.updateRow i b).conjTranspose
@[simp]
theorem Matrix.updateRow_eq_self {m : Type u_2} {n : Type u_3} {α : Type v} [] (A : Matrix m n α) (i : m) :
A.updateRow i (A i) = A
@[simp]
theorem Matrix.updateColumn_eq_self {m : Type u_2} {n : Type u_3} {α : Type v} [] (A : Matrix m n α) (i : n) :
(A.updateColumn i fun (j : m) => A j i) = A
theorem Matrix.diagonal_updateColumn_single {n : Type u_3} {α : Type v} [] [Zero α] (v : nα) (i : n) (x : α) :
().updateColumn i () = Matrix.diagonal ()
theorem Matrix.diagonal_updateRow_single {n : Type u_3} {α : Type v} [] [Zero α] (v : nα) (i : n) (x : α) :
().updateRow i () = Matrix.diagonal ()

Updating rows and columns commutes in the obvious way with reindexing the matrix.

theorem Matrix.updateRow_submatrix_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [] [] (A : Matrix m n α) (i : l) (r : oα) (e : l m) (f : o n) :
(A.submatrix e f).updateRow i r = (A.updateRow (e i) fun (j : n) => r (f.symm j)).submatrix e f
theorem Matrix.submatrix_updateRow_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [] [] (A : Matrix m n α) (i : m) (r : nα) (e : l m) (f : o n) :
(A.updateRow i r).submatrix e f = (A.submatrix e f).updateRow (e.symm i) fun (i : o) => r (f i)
theorem Matrix.updateColumn_submatrix_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [] [] (A : Matrix m n α) (j : o) (c : lα) (e : l m) (f : o n) :
(A.submatrix e f).updateColumn j c = (A.updateColumn (f j) fun (i : m) => c (e.symm i)).submatrix e f
theorem Matrix.submatrix_updateColumn_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [] [] (A : Matrix m n α) (j : n) (c : mα) (e : l m) (f : o n) :
(A.updateColumn j c).submatrix e f = (A.submatrix e f).updateColumn (f.symm j) fun (i : l) => c (e i)

reindex versions of the above submatrix lemmas for convenience.

theorem Matrix.updateRow_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [] [] (A : Matrix m n α) (i : l) (r : oα) (e : m l) (f : n o) :
(() A).updateRow i r = () (A.updateRow (e.symm i) fun (j : n) => r (f j))
theorem Matrix.reindex_updateRow {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [] [] (A : Matrix m n α) (i : m) (r : nα) (e : m l) (f : n o) :
() (A.updateRow i r) = (() A).updateRow (e i) fun (i : o) => r (f.symm i)
theorem Matrix.updateColumn_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [] [] (A : Matrix m n α) (j : o) (c : lα) (e : m l) (f : n o) :
(() A).updateColumn j c = () (A.updateColumn (f.symm j) fun (i : m) => c (e i))
theorem Matrix.reindex_updateColumn {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [] [] (A : Matrix m n α) (j : n) (c : mα) (e : m l) (f : n o) :
() (A.updateColumn j c) = (() A).updateColumn (f j) fun (i : l) => c (e.symm i)