Row and column matrices #

This file provides results about row and column matrices.

Main definitions #

Matrix.replicateRow ι r : Matrix ι n α: the matrix where every row is the vector r : n → α
Matrix.replicateCol ι c : Matrix m ι α: the matrix where every column is the vector c : m → α
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

source

def Matrix.replicateCol {m : Type u_2} {α : Type v} (ι : Type u_6) (w : m → α) :

Matrix m ι α

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

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

Equations

Matrix.replicateCol ι w = Matrix.of fun (x : m) (x_1 : ι) => w x

Instances For

source

@[simp]

theorem Matrix.replicateCol_apply {m : Type u_2} {α : Type v} {ι : Type u_6} (w : m → α) (i : m) (j : ι) :

replicateCol ι w i j = w i

source

def Matrix.replicateRow {n : Type u_3} {α : Type v} (ι : Type u_6) (v : n → α) :

Matrix ι n α

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

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

Equations

Matrix.replicateRow ι v = Matrix.of fun (x : ι) (y : n) => v y

Instances For

source

@[simp]

theorem Matrix.replicateRow_apply {n : Type u_3} {α : Type v} {ι : Type u_6} (v : n → α) (i : ι) (j : n) :

replicateRow ι v i j = v j

source

@[simp]

theorem Matrix.vecMulVec_one {m : Type u_2} {n : Type u_3} {R : Type u_5} [MulOneClass R] (x : n → R) :

vecMulVec x 1 = replicateCol m x

source

@[simp]

theorem Matrix.one_vecMulVec {m : Type u_2} {n : Type u_3} {R : Type u_5} [MulOneClass R] (x : n → R) :

vecMulVec 1 x = replicateRow m x

source

theorem Matrix.replicateCol_injective {m : Type u_2} {α : Type v} {ι : Type u_6} [Nonempty ι] :

Function.Injective (replicateCol ι)

source

@[deprecated Matrix.replicateCol_injective (since := "2025-03-20")]

theorem Matrix.col_injective {m : Type u_2} {α : Type v} {ι : Type u_6} [Nonempty ι] :

Function.Injective (replicateCol ι)

Alias of Matrix.replicateCol_injective.

source

@[simp]

theorem Matrix.replicateCol_inj {m : Type u_2} {α : Type v} {ι : Type u_6} [Nonempty ι] {v w : m → α} :

replicateCol ι v = replicateCol ι w ↔ v = w

source

@[deprecated Matrix.replicateCol_inj (since := "2025-03-20")]

theorem Matrix.col_inj {m : Type u_2} {α : Type v} {ι : Type u_6} [Nonempty ι] {v w : m → α} :

replicateCol ι v = replicateCol ι w ↔ v = w

Alias of Matrix.replicateCol_inj.

source

@[simp]

theorem Matrix.replicateCol_zero {m : Type u_2} {α : Type v} {ι : Type u_6} [Zero α] :

replicateCol ι 0 = 0

source

@[deprecated Matrix.replicateCol_zero (since := "2025-03-20")]

theorem Matrix.col_zero {m : Type u_2} {α : Type v} {ι : Type u_6} [Zero α] :

replicateCol ι 0 = 0

Alias of Matrix.replicateCol_zero.

source

@[simp]

theorem Matrix.replicateCol_eq_zero {m : Type u_2} {α : Type v} {ι : Type u_6} [Zero α] [Nonempty ι] (v : m → α) :

replicateCol ι v = 0 ↔ v = 0

source

@[deprecated Matrix.replicateCol_eq_zero (since := "2025-03-20")]

theorem Matrix.col_eq_zero {m : Type u_2} {α : Type v} {ι : Type u_6} [Zero α] [Nonempty ι] (v : m → α) :

replicateCol ι v = 0 ↔ v = 0

Alias of Matrix.replicateCol_eq_zero.

source

@[simp]

theorem Matrix.replicateCol_add {m : Type u_2} {α : Type v} {ι : Type u_6} [Add α] (v w : m → α) :

replicateCol ι (v + w) = replicateCol ι v + replicateCol ι w

source

@[deprecated Matrix.replicateCol_add (since := "2025-03-20")]

theorem Matrix.col_add {m : Type u_2} {α : Type v} {ι : Type u_6} [Add α] (v w : m → α) :

replicateCol ι (v + w) = replicateCol ι v + replicateCol ι w

Alias of Matrix.replicateCol_add.

source

@[simp]

theorem Matrix.replicateCol_smul {m : Type u_2} {R : Type u_5} {α : Type v} {ι : Type u_6} [SMul R α] (x : R) (v : m → α) :

replicateCol ι (x • v) = x • replicateCol ι v

source

@[deprecated Matrix.replicateCol_smul (since := "2025-03-20")]

theorem Matrix.col_smul {m : Type u_2} {R : Type u_5} {α : Type v} {ι : Type u_6} [SMul R α] (x : R) (v : m → α) :

replicateCol ι (x • v) = x • replicateCol ι v

Alias of Matrix.replicateCol_smul.

source

theorem Matrix.replicateRow_injective {n : Type u_3} {α : Type v} {ι : Type u_6} [Nonempty ι] :

Function.Injective (replicateRow ι)

source

@[deprecated Matrix.replicateRow_injective (since := "2025-03-20")]

theorem Matrix.row_injective {n : Type u_3} {α : Type v} {ι : Type u_6} [Nonempty ι] :

Function.Injective (replicateRow ι)

Alias of Matrix.replicateRow_injective.

source

@[simp]

theorem Matrix.replicateRow_inj {n : Type u_3} {α : Type v} {ι : Type u_6} [Nonempty ι] {v w : n → α} :

replicateRow ι v = replicateRow ι w ↔ v = w

source

@[simp]

theorem Matrix.replicateRow_zero {n : Type u_3} {α : Type v} {ι : Type u_6} [Zero α] :

replicateRow ι 0 = 0

source

@[deprecated Matrix.replicateRow_zero (since := "2025-03-20")]

theorem Matrix.row_zero {n : Type u_3} {α : Type v} {ι : Type u_6} [Zero α] :

replicateRow ι 0 = 0

Alias of Matrix.replicateRow_zero.

source

@[simp]

theorem Matrix.replicateRow_eq_zero {n : Type u_3} {α : Type v} {ι : Type u_6} [Zero α] [Nonempty ι] (v : n → α) :

replicateRow ι v = 0 ↔ v = 0

source

@[deprecated Matrix.replicateRow_eq_zero (since := "2025-03-20")]

theorem Matrix.row_eq_zero {n : Type u_3} {α : Type v} {ι : Type u_6} [Zero α] [Nonempty ι] (v : n → α) :

replicateRow ι v = 0 ↔ v = 0

Alias of Matrix.replicateRow_eq_zero.

source

@[simp]

theorem Matrix.replicateRow_add {m : Type u_2} {α : Type v} {ι : Type u_6} [Add α] (v w : m → α) :

replicateRow ι (v + w) = replicateRow ι v + replicateRow ι w

source

@[deprecated Matrix.replicateRow_add (since := "2025-03-20")]

theorem Matrix.row_add {m : Type u_2} {α : Type v} {ι : Type u_6} [Add α] (v w : m → α) :

replicateRow ι (v + w) = replicateRow ι v + replicateRow ι w

Alias of Matrix.replicateRow_add.

source

@[simp]

theorem Matrix.replicateRow_smul {m : Type u_2} {R : Type u_5} {α : Type v} {ι : Type u_6} [SMul R α] (x : R) (v : m → α) :

replicateRow ι (x • v) = x • replicateRow ι v

source

@[deprecated Matrix.replicateRow_smul (since := "2025-03-20")]

theorem Matrix.row_smul {m : Type u_2} {R : Type u_5} {α : Type v} {ι : Type u_6} [SMul R α] (x : R) (v : m → α) :

replicateRow ι (x • v) = x • replicateRow ι v

Alias of Matrix.replicateRow_smul.

source

@[simp]

theorem Matrix.transpose_replicateCol {m : Type u_2} {α : Type v} {ι : Type u_6} (v : m → α) :

(replicateCol ι v).transpose = replicateRow ι v

source

@[simp]

theorem Matrix.transpose_replicateRow {m : Type u_2} {α : Type v} {ι : Type u_6} (v : m → α) :

(replicateRow ι v).transpose = replicateCol ι v

source

@[simp]

theorem Matrix.conjTranspose_replicateCol {m : Type u_2} {α : Type v} {ι : Type u_6} [Star α] (v : m → α) :

(replicateCol ι v).conjTranspose = replicateRow ι (star v)

source

@[deprecated Matrix.conjTranspose_replicateCol (since := "2025-03-20")]

theorem Matrix.conjTranspose_col {m : Type u_2} {α : Type v} {ι : Type u_6} [Star α] (v : m → α) :

(replicateCol ι v).conjTranspose = replicateRow ι (star v)

Alias of Matrix.conjTranspose_replicateCol.

source

@[simp]

theorem Matrix.conjTranspose_replicateRow {m : Type u_2} {α : Type v} {ι : Type u_6} [Star α] (v : m → α) :

(replicateRow ι v).conjTranspose = replicateCol ι (star v)

source

@[deprecated Matrix.conjTranspose_replicateRow (since := "2025-03-20")]

theorem Matrix.conjTranspose_row {m : Type u_2} {α : Type v} {ι : Type u_6} [Star α] (v : m → α) :

(replicateRow ι v).conjTranspose = replicateCol ι (star v)

Alias of Matrix.conjTranspose_replicateRow.

source

theorem Matrix.replicateRow_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :

replicateRow ι (vecMul v M) = replicateRow ι v * M

source

@[deprecated Matrix.replicateRow_vecMul (since := "2025-03-20")]

theorem Matrix.row_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :

replicateRow ι (vecMul v M) = replicateRow ι v * M

Alias of Matrix.replicateRow_vecMul.

source

theorem Matrix.replicateCol_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :

replicateCol ι (vecMul v M) = (replicateRow ι v * M).transpose

source

@[deprecated Matrix.replicateCol_vecMul (since := "2025-03-20")]

theorem Matrix.col_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :

replicateCol ι (vecMul v M) = (replicateRow ι v * M).transpose

Alias of Matrix.replicateCol_vecMul.

source

theorem Matrix.replicateCol_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :

replicateCol ι (M.mulVec v) = M * replicateCol ι v

source

@[deprecated Matrix.replicateCol_mulVec (since := "2025-03-20")]

theorem Matrix.col_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :

replicateCol ι (M.mulVec v) = M * replicateCol ι v

Alias of Matrix.replicateCol_mulVec.

source

theorem Matrix.replicateRow_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :

replicateRow ι (M.mulVec v) = (M * replicateCol ι v).transpose

source

@[deprecated Matrix.replicateRow_mulVec (since := "2025-03-20")]

theorem Matrix.row_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :

replicateRow ι (M.mulVec v) = (M * replicateCol ι v).transpose

Alias of Matrix.replicateRow_mulVec.

source

theorem Matrix.replicateRow_mulVec_eq_const {m : Type u_2} {α : Type v} {ι : Type u_6} [Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) :

(replicateRow ι v).mulVec w = Function.const ι (v ⬝ᵥ w)

source

@[deprecated Matrix.replicateRow_mulVec_eq_const (since := "2025-03-20")]

theorem Matrix.row_mulVec_eq_const {m : Type u_2} {α : Type v} {ι : Type u_6} [Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) :

(replicateRow ι v).mulVec w = Function.const ι (v ⬝ᵥ w)

Alias of Matrix.replicateRow_mulVec_eq_const.

source

theorem Matrix.mulVec_replicateCol_eq_const {m : Type u_2} {α : Type v} {ι : Type u_6} [Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) :

vecMul v (replicateCol ι w) = Function.const ι (v ⬝ᵥ w)

source

@[deprecated Matrix.mulVec_replicateCol_eq_const (since := "2025-03-20")]

theorem Matrix.mulVec_col_eq_const {m : Type u_2} {α : Type v} {ι : Type u_6} [Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) :

vecMul v (replicateCol ι w) = Function.const ι (v ⬝ᵥ w)

Alias of Matrix.mulVec_replicateCol_eq_const.

source

theorem Matrix.replicateRow_mul_replicateCol {m : Type u_2} {α : Type v} {ι : Type u_6} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) :

replicateRow ι v * replicateCol ι w = of fun (x x : ι) => v ⬝ᵥ w

source

@[deprecated Matrix.replicateRow_mul_replicateCol (since := "2025-03-20")]

theorem Matrix.row_mul_col {m : Type u_2} {α : Type v} {ι : Type u_6} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) :

replicateRow ι v * replicateCol ι w = of fun (x x : ι) => v ⬝ᵥ w

Alias of Matrix.replicateRow_mul_replicateCol.

source

@[simp]

theorem Matrix.replicateRow_mul_replicateCol_apply {m : Type u_2} {α : Type v} {ι : Type u_6} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) (i j : ι) :

(replicateRow ι v * replicateCol ι w) i j = v ⬝ᵥ w

source

@[deprecated Matrix.replicateRow_mul_replicateCol_apply (since := "2025-03-20")]

theorem Matrix.row_mul_col_apply {m : Type u_2} {α : Type v} {ι : Type u_6} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) (i j : ι) :

(replicateRow ι v * replicateCol ι w) i j = v ⬝ᵥ w

Alias of Matrix.replicateRow_mul_replicateCol_apply.

source

@[simp]

theorem Matrix.diag_replicateCol_mul_replicateRow {n : Type u_3} {α : Type v} {ι : Type u_6} [Mul α] [AddCommMonoid α] [Unique ι] (a b : n → α) :

(replicateCol ι a * replicateRow ι b).diag = a * b

source

@[deprecated Matrix.diag_replicateCol_mul_replicateRow (since := "2025-03-20")]

theorem Matrix.diag_col_mul_row {n : Type u_3} {α : Type v} {ι : Type u_6} [Mul α] [AddCommMonoid α] [Unique ι] (a b : n → α) :

(replicateCol ι a * replicateRow ι b).diag = a * b

Alias of Matrix.diag_replicateCol_mul_replicateRow.

source

theorem Matrix.vecMulVec_eq {m : Type u_2} {n : Type u_3} {α : Type v} (ι : Type u_6) [Mul α] [AddCommMonoid α] [Unique ι] (w : m → α) (v : n → α) :

vecMulVec w v = replicateCol ι w * replicateRow ι v

Updating rows and columns #

source

def Matrix.updateRow {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] (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 (Function.update M i b)

Instances For

source

def Matrix.updateCol {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq n] (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

M.updateCol j b = Matrix.of fun (i : m) => Function.update (M i) j (b i)

Instances For

source

@[simp]

theorem Matrix.updateRow_self {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] :

M.updateRow i b i = b

source

@[simp]

theorem Matrix.updateCol_self {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [DecidableEq n] :

M.updateCol j c i j = c i

source

@[simp]

theorem Matrix.updateRow_ne {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] {i' : m} (i_ne : i' ≠ i) :

M.updateRow i b i' = M i'

source

@[simp]

theorem Matrix.updateCol_ne {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [DecidableEq n] {j' : n} (j_ne : j' ≠ j) :

M.updateCol j c i j' = M i j'

source

theorem Matrix.updateRow_apply {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {b : n → α} [DecidableEq m] {i' : m} :

M.updateRow i b i' j = if i' = i then b j else M i' j

source

theorem Matrix.updateCol_apply {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [DecidableEq n] {j' : n} :

M.updateCol j c i j' = if j' = j then c i else M i j'

source

@[simp]

theorem Matrix.updateCol_subsingleton {m : Type u_2} {n : Type u_3} {R : Type u_5} [Subsingleton n] (A : Matrix m n R) (i : n) (b : m → R) :

A.updateCol i b = (replicateCol (Fin 1) b).submatrix id (Function.const n 0)

source

@[simp]

theorem Matrix.updateRow_subsingleton {m : Type u_2} {n : Type u_3} {R : Type u_5} [Subsingleton m] (A : Matrix m n R) (i : m) (b : n → R) :

A.updateRow i b = (replicateRow (Fin 1) b).submatrix (Function.const m 0) id

source

theorem Matrix.map_updateRow {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] (f : α → β) :

(M.updateRow i b).map f = (M.map f).updateRow i (f ∘ b)

source

theorem Matrix.map_updateCol {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {j : n} {c : m → α} [DecidableEq n] (f : α → β) :

(M.updateCol j c).map f = (M.map f).updateCol j (f ∘ c)

source

theorem Matrix.updateRow_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {j : n} {c : m → α} [DecidableEq n] :

M.transpose.updateRow j c = (M.updateCol j c).transpose

source

theorem Matrix.updateCol_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] :

M.transpose.updateCol i b = (M.updateRow i b).transpose

source

theorem Matrix.updateRow_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {j : n} {c : m → α} [DecidableEq n] [Star α] :

M.conjTranspose.updateRow j (star c) = (M.updateCol j c).conjTranspose

source

theorem Matrix.updateCol_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] [Star α] :

M.conjTranspose.updateCol i (star b) = (M.updateRow i b).conjTranspose

source

@[simp]

theorem Matrix.updateRow_eq_self {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] (A : Matrix m n α) (i : m) :

A.updateRow i (A i) = A

source

@[simp]

theorem Matrix.updateCol_eq_self {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq n] (A : Matrix m n α) (i : n) :

(A.updateCol i fun (j : m) => A j i) = A

source

@[simp]

theorem Matrix.updateRow_zero_zero {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] [Zero α] (i : m) :

updateRow 0 i 0 = 0

source

@[simp]

theorem Matrix.updateCol_zero_zero {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (i : n) :

updateCol 0 i 0 = 0

source

theorem Matrix.diagonal_updateCol_single {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :

(diagonal v).updateCol i (Pi.single i x) = diagonal (Function.update v i x)

source

theorem Matrix.diagonal_updateRow_single {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :

(diagonal v).updateRow i (Pi.single i x) = diagonal (Function.update v i x)

source

@[simp]

theorem Matrix.updateRow_idem {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] (A : Matrix m n α) (i : m) (x y : n → α) :

(A.updateRow i x).updateRow i y = A.updateRow i y

source

theorem Matrix.updateRow_comm {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] (A : Matrix m n α) {i i' : m} (h : i ≠ i') (x y : n → α) :

(A.updateRow i x).updateRow i' y = (A.updateRow i' y).updateRow i x

source

@[simp]

theorem Matrix.updateCol_idem {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq n] (A : Matrix m n α) (j : n) (x y : m → α) :

(A.updateCol j x).updateCol j y = A.updateCol j y

source

theorem Matrix.updateCol_comm {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq n] (A : Matrix m n α) {j j' : n} (h : j ≠ j') (x y : m → α) :

(A.updateCol j x).updateCol j' y = (A.updateCol j' y).updateCol j x

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

source

theorem Matrix.updateRow_submatrix_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq l] [DecidableEq m] (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

source

theorem Matrix.submatrix_updateRow_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq l] [DecidableEq m] (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)

source

theorem Matrix.updateCol_submatrix_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : l ≃ m) (f : o ≃ n) :

(A.submatrix ⇑e ⇑f).updateCol j c = (A.updateCol (f j) fun (i : m) => c (e.symm i)).submatrix ⇑e ⇑f

source

theorem Matrix.submatrix_updateCol_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : n) (c : m → α) (e : l ≃ m) (f : o ≃ n) :

(A.updateCol j c).submatrix ⇑e ⇑f = (A.submatrix ⇑e ⇑f).updateCol (f.symm j) fun (i : l) => c (e i)

reindex versions of the above submatrix lemmas for convenience.

source

theorem Matrix.updateRow_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : m ≃ l) (f : n ≃ o) :

((reindex e f) A).updateRow i r = (reindex e f) (A.updateRow (e.symm i) fun (j : n) => r (f j))

source

theorem Matrix.reindex_updateRow {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : m) (r : n → α) (e : m ≃ l) (f : n ≃ o) :

(reindex e f) (A.updateRow i r) = ((reindex e f) A).updateRow (e i) fun (i : o) => r (f.symm i)

source

theorem Matrix.updateCol_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : m ≃ l) (f : n ≃ o) :

((reindex e f) A).updateCol j c = (reindex e f) (A.updateCol (f.symm j) fun (i : m) => c (e i))

source

theorem Matrix.reindex_updateCol {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : n) (c : m → α) (e : m ≃ l) (f : n ≃ o) :

(reindex e f) (A.updateCol j c) = ((reindex e f) A).updateCol (f j) fun (i : l) => c (e.symm i)

source

theorem Matrix.single_eq_updateRow_zero {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (r : α) :

single i j r = updateRow 0 i (Pi.single j r)

source

theorem Matrix.single_eq_updateCol_zero {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (r : α) :

single i j r = updateCol 0 j (Pi.single i r)

source

theorem Matrix.updateRow_mulVec {l : Type u_1} {m : Type u_2} {α : Type v} [DecidableEq l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix l m α) (i : l) (c v : m → α) :

(A.updateRow i c).mulVec v = Function.update (A.mulVec v) i (c ⬝ᵥ v)

source

theorem Matrix.vecMul_updateCol {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) (B : Matrix m n α) (j : n) (r : m → α) :

vecMul v (B.updateCol j r) = Function.update (vecMul v B) j (v ⬝ᵥ r)

source

theorem Matrix.update_vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] [Mul α] (u : m → α) (v : n → α) (i : m) (a : α) :

vecMulVec (Function.update u i a) v = (vecMulVec u v).updateRow i (a • v)

source

theorem Matrix.vecMulVec_update {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq n] [Mul α] (u : m → α) (v : n → α) (j : n) (a : α) :

vecMulVec u (Function.update v j a) = (vecMulVec u v).updateCol j (MulOpposite.op a • u)

source

theorem Matrix.updateRow_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix l m α) (i : l) (r : m → α) (B : Matrix m n α) :

A.updateRow i r * B = (A * B).updateRow i (vecMul r B)

source

theorem Matrix.mul_updateCol {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix l m α) (B : Matrix m n α) (j : n) (c : m → α) :

A * B.updateCol j c = (A * B).updateCol j (A.mulVec c)

source

theorem Matrix.mul_single_eq_updateCol_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix l m α) (i : m) (j : n) (r : α) :

A * single i j r = updateCol 0 j (MulOpposite.op r • A.col i)

source

theorem Matrix.single_mul_eq_updateRow_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq l] [DecidableEq m] [Fintype m] [NonUnitalNonAssocSemiring α] (i : l) (j : m) (r : α) (B : Matrix m n α) :

single i j r * B = updateRow 0 i (r • B.row j)

source

@[simp]

theorem Matrix.updateRow_zero_mul_updateCol_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq l] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (i : l) (r : m → α) (j : n) (c : m → α) :

updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)

Documentation

Mathlib.LinearAlgebra.Matrix.RowCol

Row and column matrices #

Main definitions #

Updating rows and columns #