Algebraic laws for dense matrix multiplication.

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.

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

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