@[simp]

theorem Hex.Matrix.mulVec_unit {R : Type u_1} {n m : Nat} [Lean.Grind.CommRing R] (M : Matrix R n m) (j : Fin m) : M * Vector.unit R j = M.col j

Multiplication by a standard basis vector selects the corresponding matrix column.

theorem Hex.Matrix.mul_assoc_vec {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (B : Matrix R m k) (v : Vector R k) : A * B * v = A * (B * v)

Matrix multiplication associates with matrix-vector multiplication.

theorem Hex.Matrix.transpose_mul_of_mul_comm {R : Type u_1} {n m k : Nat} [Lean.Grind.CommRing R] (A : Matrix R n m) (B : Matrix R m k) : (A * B).transpose = B.transpose * A.transpose

Transpose reverses matrix multiplication over a commutative coefficient type.

theorem Hex.Matrix.vecMul_mul {R : Type u_1} {n m k : Nat} [Lean.Grind.CommRing R] (v : Vector R n) (A : Matrix R n m) (B : Matrix R m k) : vecMul (vecMul v A) B = vecMul v (A * B)

Row-vector multiplication associates with matrix multiplication.

theorem Hex.Matrix.vecMul_ofRows {R : Type u_1} {n m : Nat} [Lean.Grind.CommRing R] (c : Vector R n) (rows : Vector (Vector R m) n) : vecMul c (ofRows rows) = List.foldl (fun (acc : Vector R m) (i : Fin n) => acc + c[i] • rows[i]) 0 (List.finRange n)

A row-vector product with a matrix assembled from rows is the corresponding linear combination of those rows.

theorem Hex.Matrix.vecMul_assoc {R : Type u_1} {n m k : Nat} [Lean.Grind.CommRing R] (v : Vector R n) (A : Matrix R n m) (B : Matrix R m k) : v * A * B = v * (A * B)

Row-vector multiplication associates with matrix multiplication.

theorem Hex.Matrix.getElem_vecMul_diagMatrix {R : Type u_1} [Lean.Grind.CommRing R] {r n m : Nat} (d : Vector R r) (v : Vector R n) (hrn : r ≤ n) (j : Fin m) : (v * diagMatrix d n m)[j] = if h : ↑j < r then d[↑j] * v[↑j] else 0

A row vector times a rectangular leading-diagonal matrix, entrywise.

@[simp]

theorem Hex.Matrix.identity_mulVec {R : Type u_1} {n : Nat} [Lean.Grind.Ring R] (v : Vector R n) : Matrix.identity n * v = v

Left-multiplication by the identity matrix leaves a vector unchanged.

@[simp]

theorem Hex.Matrix.vecMul_identity {R : Type u_1} {n : Nat} [Lean.Grind.CommRing R] (v : Vector R n) : vecMul v (Matrix.identity n) = v

Right-multiplication of a row vector by the identity leaves it unchanged.

@[simp]

theorem Hex.Matrix.identity_mul {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (M : Matrix R n m) : Matrix.identity n * M = M

Left-multiplication by the identity matrix leaves a matrix unchanged.

@[simp]

theorem Hex.Matrix.mul_identity {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (M : Matrix R n m) : M * Matrix.identity m = M

Right-multiplication by the identity matrix leaves a matrix unchanged.

theorem Hex.Matrix.mul_assoc {R : Type u_1} {n m k l : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (B : Matrix R m k) (C : Matrix R k l) : A * B * C = A * (B * C)

Matrix multiplication is associative.

theorem Hex.Matrix.row_mul_eq_zero {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (B : Matrix R m k) (i : Fin n) (hrow : A.row i = 0) : (A * B).row i = 0

A zero row remains zero after right matrix multiplication.

@[simp]

theorem Hex.Matrix.mulVec_zero {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) : A * 0 = 0

Matrix-vector multiplication sends the zero vector to the zero vector.

@[simp]

theorem Hex.Matrix.mulVec_add {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (u v : Vector R m) : A * (u + v) = A * u + A * v

Matrix-vector multiplication is additive in the vector.

@[simp]

theorem Hex.Matrix.mulVec_smul {R : Type u_1} {n m : Nat} [Lean.Grind.CommRing R] (A : Matrix R n m) (c : R) (v : Vector R m) : A * c • v = c • (A * v)

Matrix-vector multiplication commutes with scalar multiplication.

@[simp]

theorem Hex.Matrix.vecMul_add {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (u v : Vector R n) (A : Matrix R n m) : vecMul (u + v) A = vecMul u A + vecMul v A

Row-vector multiplication is additive in the row vector.

@[simp]

theorem Hex.Matrix.vecMul_smul {R : Type u_1} {n m : Nat} [Lean.Grind.CommRing R] (c : R) (v : Vector R n) (A : Matrix R n m) : vecMul (c • v) A = c • vecMul v A

Row-vector multiplication commutes with scalar multiplication.

@[simp]

theorem Hex.Matrix.vecMul_zero {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) : vecMul 0 A = 0

The zero row vector multiplies every matrix to zero.

@[simp]

theorem Hex.Matrix.zero_mulVec {R : Type u_1} {m n : Nat} [Lean.Grind.Ring R] (v : Vector R m) : 0 * v = 0

The zero matrix sends every vector to the zero vector.

theorem Hex.Matrix.sub_mulVec {R : Type u_1} {n m : Nat} [Lean.Grind.Ring R] (A B : Matrix R n m) (v : Vector R m) : (A - B) * v = A * v - B * v

Matrix-vector multiplication distributes over matrix subtraction.

theorem Hex.Matrix.sub_identity_mulVec {R : Type u_1} {n : Nat} [Lean.Grind.Ring R] (Q : Matrix R n n) (v : Vector R n) : (Q - Matrix.identity n) * v = Q * v - v

Multiplication by Q - I is Q * v - v.

@[simp]

theorem Hex.Matrix.row_add {R : Type u_1} {n m : Nat} [Add R] (A B : Matrix R n m) (i : Fin n) : (A + B).row i = A.row i + B.row i

The i-th row of a matrix sum is the sum of the rows.

@[simp]

theorem Hex.Matrix.row_sub {R : Type u_1} {n m : Nat} [Sub R] (A B : Matrix R n m) (i : Fin n) : (A - B).row i = A.row i - B.row i

The i-th row of a matrix difference is the difference of the rows.

@[simp]

theorem Hex.Matrix.col_add {R : Type u_1} {n m : Nat} [Add R] (A B : Matrix R n m) (j : Fin m) : (A + B).col j = A.col j + B.col j

The j-th column of a matrix sum is the sum of the columns.

@[simp]

theorem Hex.Matrix.col_sub {R : Type u_1} {n m : Nat} [Sub R] (A B : Matrix R n m) (j : Fin m) : (A - B).col j = A.col j - B.col j

The j-th column of a matrix difference is the difference of the columns.

theorem Hex.Matrix.add_mul {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (A B : Matrix R n m) (C : Matrix R m k) : (A + B) * C = A * C + B * C

Matrix multiplication distributes over addition on the left.

theorem Hex.Matrix.mul_add {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (B C : Matrix R m k) : A * (B + C) = A * B + A * C

Matrix multiplication distributes over addition on the right.

theorem Hex.Matrix.sub_mul {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (A B : Matrix R n m) (C : Matrix R m k) : (A - B) * C = A * C - B * C

Matrix multiplication distributes over subtraction on the left.

theorem Hex.Matrix.mul_sub {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (B C : Matrix R m k) : A * (B - C) = A * B - A * C

Matrix multiplication distributes over subtraction on the right.

@[simp]

theorem Hex.Matrix.row_smul {R : Type u_1} {n m : Nat} {S : Type v} [SMul S R] (c : S) (M : Matrix R n m) (i : Fin n) : (c • M).row i = c • M.row i

Row i of a scalar multiple is the scalar multiple of row i.

theorem Hex.Matrix.smul_mul {R : Type u_1} {n m k : Nat} [Lean.Grind.Ring R] (c : R) (A : Matrix R n m) (B : Matrix R m k) : c • A * B = c • (A * B)

Scalar multiplication commutes with matrix multiplication on the left.

Together with mul_adjugate and adjugate_mul this is what turns a one-sided matrix inverse into a two-sided one; see HexDeterminant.mul_eq_one_comm.