Matrix multiplication

This file defines vector and matrix multiplication

Main definitions

• dotProduct: the dot product between two vectors
• Matrix.mul: multiplication of two matrices
• Matrix.mulVec: multiplication of a matrix with a vector
• Matrix.vecMul: multiplication of a vector with a matrix
• Matrix.vecMulVec: multiplication of a vector with a vector to get a matrix
• Matrix.instRing: square matrices form a ring

Notation

The locale Matrix gives the following notation:

• ⬝ᵥ for dotProduct
• *ᵥ for Matrix.mulVec
• ᵥ* for Matrix.vecMul

See Mathlib/Data/Matrix/ConjTranspose.lean for

• ᴴ for Matrix.conjTranspose

Implementation notes

For convenience, Matrix m n α is defined as m → n → α, as this allows elements of the matrix to be accessed with A i j. However, it is not advisable to construct matrices using terms of the form fun i j ↦ _ or even (fun i j ↦ _ : Matrix m n α), as these are not recognized by Lean as having the right type. Instead, Matrix.of should be used.

TODO

Under various conditions, multiplication of infinite matrices makes sense. These have not yet been implemented.

def dotProduct {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α

dotProduct v w is the sum of the entrywise products v i * w i

Equations

• v ⬝ᵥ w = ∑ i : m, v i * w i

@[deprecated dotProduct (since := "2024-12-12")]

def Matrix.dotProduct {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : α

Alias of dotProduct.

---

dotProduct v w is the sum of the entrywise products v i * w i

Equations

• @Matrix.dotProduct = @dotProduct

def «term_⬝ᵥ_» : Lean.TrailingParserDescr

dotProduct v w is the sum of the entrywise products v i * w i

Equations

• «term_⬝ᵥ_» = Lean.ParserDescr.trailingNode `«term_⬝ᵥ_» 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⬝ᵥ ") (Lean.ParserDescr.cat `term 73))

theorem dotProduct_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalSemiring α] (u : m → α) (w : n → α) (v : Matrix m n α) : (fun (j : n) => u ⬝ᵥ fun (i : m) => v i j) ⬝ᵥ w = u ⬝ᵥ fun (i : m) => v i ⬝ᵥ w

@[deprecated dotProduct_assoc (since := "2024-12-12")]

theorem Matrix.dotProduct_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalSemiring α] (u : m → α) (w : n → α) (v : Matrix m n α) : (fun (j : n) => u ⬝ᵥ fun (i : m) => v i j) ⬝ᵥ w = u ⬝ᵥ fun (i : m) => v i ⬝ᵥ w

Alias of dotProduct_assoc.

theorem dotProduct_comm {m : Type u_2} {α : Type v} [Fintype m] [AddCommMonoid α] [CommMagma α] (v w : m → α) : v ⬝ᵥ w = w ⬝ᵥ v

@[deprecated dotProduct_comm (since := "2024-12-12")]

theorem Matrix.dotProduct_comm {m : Type u_2} {α : Type v} [Fintype m] [AddCommMonoid α] [CommMagma α] (v w : m → α) : v ⬝ᵥ w = w ⬝ᵥ v

Alias of dotProduct_comm.

@[simp]

theorem dotProduct_pUnit {α : Type v} [AddCommMonoid α] [Mul α] (v w : PUnit.{u_10 + 1} → α) : v ⬝ᵥ w = v PUnit.unit * w PUnit.unit

@[deprecated dotProduct_pUnit (since := "2024-12-12")]

theorem Matrix.dotProduct_pUnit {α : Type v} [AddCommMonoid α] [Mul α] (v w : PUnit.{u_10 + 1} → α) : v ⬝ᵥ w = v PUnit.unit * w PUnit.unit

Alias of dotProduct_pUnit.

theorem dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : n → α) : v ⬝ᵥ 1 = ∑ i : n, v i

@[deprecated dotProduct_one (since := "2024-12-12")]

theorem Matrix.dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : n → α) : v ⬝ᵥ 1 = ∑ i : n, v i

Alias of dotProduct_one.

theorem one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : n → α) : 1 ⬝ᵥ v = ∑ i : n, v i

@[deprecated one_dotProduct (since := "2024-12-12")]

theorem Matrix.one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : n → α) : 1 ⬝ᵥ v = ∑ i : n, v i

Alias of one_dotProduct.

@[simp]

theorem dotProduct_zero {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : v ⬝ᵥ 0 = 0

@[deprecated dotProduct_zero (since := "2024-12-12")]

theorem Matrix.dotProduct_zero {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : v ⬝ᵥ 0 = 0

Alias of dotProduct_zero.

@[simp]

theorem dotProduct_zero' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : (v ⬝ᵥ fun (x : m) => 0) = 0

@[deprecated dotProduct_zero' (since := "2024-12-12")]

theorem Matrix.dotProduct_zero' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : (v ⬝ᵥ fun (x : m) => 0) = 0

Alias of dotProduct_zero'.

@[simp]

theorem zero_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : 0 ⬝ᵥ v = 0

@[deprecated zero_dotProduct (since := "2024-12-12")]

theorem Matrix.zero_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : 0 ⬝ᵥ v = 0

Alias of zero_dotProduct.

@[simp]

theorem zero_dotProduct' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : (fun (x : m) => 0) ⬝ᵥ v = 0

@[deprecated zero_dotProduct' (since := "2024-12-12")]

theorem Matrix.zero_dotProduct' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) : (fun (x : m) => 0) ⬝ᵥ v = 0

Alias of zero_dotProduct'.

@[simp]

theorem add_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u v w : m → α) : (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w

@[deprecated add_dotProduct (since := "2024-12-12")]

theorem Matrix.add_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u v w : m → α) : (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w

Alias of add_dotProduct.

@[simp]

theorem dotProduct_add {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u v w : m → α) : u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w

@[deprecated dotProduct_add (since := "2024-12-12")]

theorem Matrix.dotProduct_add {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u v w : m → α) : u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w

Alias of dotProduct_add.

@[simp]

theorem sumElim_dotProduct_sumElim {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u v : m → α) (x y : n → α) : Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y

@[deprecated sumElim_dotProduct_sumElim (since := "2024-12-12")]

theorem Matrix.sum_elim_dotProduct_sum_elim {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u v : m → α) (x y : n → α) : Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y

Alias of sumElim_dotProduct_sumElim.

@[deprecated sumElim_dotProduct_sumElim (since := "2025-02-21")]

theorem sum_elim_dotProduct_sum_elim {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u v : m → α) (x y : n → α) : Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y

Alias of sumElim_dotProduct_sumElim.

@[simp]

theorem comp_equiv_symm_dotProduct {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : m → α) (x : n → α) (e : m ≃ n) : u ∘ ⇑e.symm ⬝ᵥ x = u ⬝ᵥ x ∘ ⇑e

Permuting a vector on the left of a dot product can be transferred to the right.

@[deprecated comp_equiv_symm_dotProduct (since := "2024-12-12")]

theorem Matrix.comp_equiv_symm_dotProduct {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : m → α) (x : n → α) (e : m ≃ n) : u ∘ ⇑e.symm ⬝ᵥ x = u ⬝ᵥ x ∘ ⇑e

Alias of comp_equiv_symm_dotProduct.

---

Permuting a vector on the left of a dot product can be transferred to the right.

@[simp]

theorem dotProduct_comp_equiv_symm {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : m → α) (x : n → α) (e : n ≃ m) : u ⬝ᵥ x ∘ ⇑e.symm = u ∘ ⇑e ⬝ᵥ x

Permuting a vector on the right of a dot product can be transferred to the left.

@[deprecated dotProduct_comp_equiv_symm (since := "2024-12-12")]

theorem Matrix.dotProduct_comp_equiv_symm {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : m → α) (x : n → α) (e : n ≃ m) : u ⬝ᵥ x ∘ ⇑e.symm = u ∘ ⇑e ⬝ᵥ x

Alias of dotProduct_comp_equiv_symm.

---

Permuting a vector on the right of a dot product can be transferred to the left.

@[simp]

theorem comp_equiv_dotProduct_comp_equiv {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (x y : n → α) (e : m ≃ n) : x ∘ ⇑e ⬝ᵥ y ∘ ⇑e = x ⬝ᵥ y

Permuting vectors on both sides of a dot product is a no-op.

@[deprecated comp_equiv_dotProduct_comp_equiv (since := "2024-12-12")]

theorem Matrix.comp_equiv_dotProduct_comp_equiv {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (x y : n → α) (e : m ≃ n) : x ∘ ⇑e ⬝ᵥ y ∘ ⇑e = x ⬝ᵥ y

Alias of comp_equiv_dotProduct_comp_equiv.

---

Permuting vectors on both sides of a dot product is a no-op.

@[simp]

theorem diagonal_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : m → α) (i : m) : Matrix.diagonal v i ⬝ᵥ w = v i * w i

@[deprecated diagonal_dotProduct (since := "2024-12-12")]

theorem Matrix.diagonal_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : m → α) (i : m) : diagonal v i ⬝ᵥ w = v i * w i

Alias of diagonal_dotProduct.

@[simp]

theorem dotProduct_diagonal {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : m → α) (i : m) : v ⬝ᵥ Matrix.diagonal w i = v i * w i

@[deprecated dotProduct_diagonal (since := "2024-12-12")]

theorem Matrix.dotProduct_diagonal {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : m → α) (i : m) : v ⬝ᵥ diagonal w i = v i * w i

Alias of dotProduct_diagonal.

@[simp]

theorem dotProduct_diagonal' {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : m → α) (i : m) : (v ⬝ᵥ fun (j : m) => Matrix.diagonal w j i) = v i * w i

@[deprecated dotProduct_diagonal' (since := "2024-12-12")]

theorem Matrix.dotProduct_diagonal' {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : m → α) (i : m) : (v ⬝ᵥ fun (j : m) => diagonal w j i) = v i * w i

Alias of dotProduct_diagonal'.

@[simp]

theorem single_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (x : α) (i : m) : Pi.single i x ⬝ᵥ v = x * v i

@[deprecated single_dotProduct (since := "2024-12-12")]

theorem Matrix.single_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (x : α) (i : m) : Pi.single i x ⬝ᵥ v = x * v i

Alias of single_dotProduct.

@[simp]

theorem dotProduct_single {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (x : α) (i : m) : v ⬝ᵥ Pi.single i x = v i * x

@[deprecated dotProduct_single (since := "2024-12-12")]

theorem Matrix.dotProduct_single {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (x : α) (i : m) : v ⬝ᵥ Pi.single i x = v i * x

Alias of dotProduct_single.

@[simp]

theorem one_dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] : 1 ⬝ᵥ 1 = ↑(Fintype.card n)

@[deprecated one_dotProduct_one (since := "2024-12-12")]

theorem Matrix.one_dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] : 1 ⬝ᵥ 1 = ↑(Fintype.card n)

Alias of one_dotProduct_one.

theorem dotProduct_single_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] [DecidableEq n] (v : n → α) (i : n) : v ⬝ᵥ Pi.single i 1 = v i

@[deprecated dotProduct_single_one (since := "2024-12-12")]

theorem Matrix.dotProduct_single_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] [DecidableEq n] (v : n → α) (i : n) : v ⬝ᵥ Pi.single i 1 = v i

Alias of dotProduct_single_one.

theorem single_one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] [DecidableEq n] (i : n) (v : n → α) : Pi.single i 1 ⬝ᵥ v = v i

@[deprecated single_one_dotProduct (since := "2024-12-12")]

theorem Matrix.single_one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] [DecidableEq n] (i : n) (v : n → α) : Pi.single i 1 ⬝ᵥ v = v i

Alias of single_one_dotProduct.

@[simp]

theorem neg_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : m → α) : -v ⬝ᵥ w = -(v ⬝ᵥ w)

@[deprecated neg_dotProduct (since := "2024-12-12")]

theorem Matrix.neg_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : m → α) : -v ⬝ᵥ w = -(v ⬝ᵥ w)

Alias of neg_dotProduct.

@[simp]

theorem dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : m → α) : v ⬝ᵥ -w = -(v ⬝ᵥ w)

@[deprecated dotProduct_neg (since := "2024-12-12")]

theorem Matrix.dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : m → α) : v ⬝ᵥ -w = -(v ⬝ᵥ w)

Alias of dotProduct_neg.

theorem neg_dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : m → α) : -v ⬝ᵥ -w = v ⬝ᵥ w

@[deprecated neg_dotProduct_neg (since := "2024-12-12")]

theorem Matrix.neg_dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : m → α) : -v ⬝ᵥ -w = v ⬝ᵥ w

Alias of neg_dotProduct_neg.

@[simp]

theorem sub_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u v w : m → α) : (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w

@[deprecated sub_dotProduct (since := "2024-12-12")]

theorem Matrix.sub_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u v w : m → α) : (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w

Alias of sub_dotProduct.

@[simp]

theorem dotProduct_sub {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u v w : m → α) : u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w

@[deprecated dotProduct_sub (since := "2024-12-12")]

theorem Matrix.dotProduct_sub {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u v w : m → α) : u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w

Alias of dotProduct_sub.

@[simp]

theorem smul_dotProduct {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [Monoid R] [Mul α] [AddCommMonoid α] [DistribMulAction R α] [IsScalarTower R α α] (x : R) (v w : m → α) : x • v ⬝ᵥ w = x • (v ⬝ᵥ w)

@[deprecated smul_dotProduct (since := "2024-12-12")]

theorem Matrix.smul_dotProduct {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [Monoid R] [Mul α] [AddCommMonoid α] [DistribMulAction R α] [IsScalarTower R α α] (x : R) (v w : m → α) : x • v ⬝ᵥ w = x • (v ⬝ᵥ w)

Alias of smul_dotProduct.

@[simp]

theorem dotProduct_smul {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [Monoid R] [Mul α] [AddCommMonoid α] [DistribMulAction R α] [SMulCommClass R α α] (x : R) (v w : m → α) : v ⬝ᵥ x • w = x • (v ⬝ᵥ w)

@[deprecated dotProduct_smul (since := "2024-12-12")]

theorem Matrix.dotProduct_smul {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [Monoid R] [Mul α] [AddCommMonoid α] [DistribMulAction R α] [SMulCommClass R α α] (x : R) (v w : m → α) : v ⬝ᵥ x • w = x • (v ⬝ᵥ w)

Alias of dotProduct_smul.

@[defaultInstance 100]

instance Matrix.instHMulOfFintypeOfMulOfAddCommMonoid {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] : HMul (Matrix l m α) (Matrix m n α) (Matrix l n α)

M * N is the usual product of matrices M and N, i.e. we have that (M * N) i k is the dot product of the i-th row of M by the k-th column of N. This is currently only defined when m is finite.

Equations

• Matrix.instHMulOfFintypeOfMulOfAddCommMonoid = { hMul := fun (M : Matrix l m α) (N : Matrix m n α) (i : l) (k : n) => (fun (j : m) => M i j) ⬝ᵥ fun (j : m) => N j k }

theorem Matrix.mul_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i : l} {k : n} : (M * N) i k = ∑ j : m, M i j * N j k

instance Matrix.instMulOfFintypeOfAddCommMonoid {n : Type u_3} {α : Type v} [Fintype n] [Mul α] [AddCommMonoid α] : Mul (Matrix n n α)

Equations

• Matrix.instMulOfFintypeOfAddCommMonoid = { mul := fun (M N : Matrix n n α) => M * N }

theorem Matrix.mul_apply' {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i : l} {k : n} : (M * N) i k = (fun (j : m) => M i j) ⬝ᵥ fun (j : m) => N j k

theorem Matrix.two_mul_expl {R : Type u_10} [NonUnitalNonAssocSemiring R] (A B : Matrix (Fin 2) (Fin 2) R) : (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧ (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧ (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

@[simp]

theorem Matrix.smul_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [AddCommMonoid α] [Mul α] [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] (a : R) (M : Matrix m n α) (N : Matrix n l α) : a • M * N = a • (M * N)

@[simp]

theorem Matrix.mul_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [AddCommMonoid α] [Mul α] [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α] (M : Matrix m n α) (a : R) (N : Matrix n l α) : M * a • N = a • (M * N)

@[simp]

theorem Matrix.mul_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (M : Matrix m n α) : M * 0 = 0

@[simp]

theorem Matrix.zero_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix m n α) : 0 * M = 0

theorem Matrix.mul_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (L : Matrix m n α) (M N : Matrix n o α) : L * (M + N) = L * M + L * N

theorem Matrix.add_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (L M : Matrix l m α) (N : Matrix m n α) : (L + M) * N = L * N + M * N

instance Matrix.nonUnitalNonAssocSemiring {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] : NonUnitalNonAssocSemiring (Matrix n n α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (d : m → α) (M : Matrix m n α) (i : m) (j : n) : (diagonal d * M) i j = d i * M i j

@[simp]

theorem Matrix.mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (d : n → α) (M : Matrix m n α) (i : m) (j : n) : (M * diagonal d) i j = M i j * d j

@[simp]

theorem Matrix.diagonal_mul_diagonal {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (d₁ d₂ : n → α) : diagonal d₁ * diagonal d₂ = diagonal fun (i : n) => d₁ i * d₂ i

theorem Matrix.diagonal_mul_diagonal' {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (d₁ d₂ : n → α) : diagonal d₁ * diagonal d₂ = diagonal fun (i : n) => d₁ i * d₂ i

theorem Matrix.smul_eq_diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (M : Matrix m n α) (a : α) : a • M = (diagonal fun (x : m) => a) * M

theorem Matrix.op_smul_eq_mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) : MulOpposite.op a • M = M * diagonal fun (x : n) => a

def Matrix.addMonoidHomMulLeft {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix l m α) : Matrix m n α →+ Matrix l n α

Left multiplication by a matrix, as an AddMonoidHom from matrices to matrices.

Equations

• M.addMonoidHomMulLeft = { toFun := fun (x : Matrix m n α) => M * x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.addMonoidHomMulLeft_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix l m α) (x : Matrix m n α) : M.addMonoidHomMulLeft x = M * x

def Matrix.addMonoidHomMulRight {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix m n α) : Matrix l m α →+ Matrix l n α

Right multiplication by a matrix, as an AddMonoidHom from matrices to matrices.

Equations

• M.addMonoidHomMulRight = { toFun := fun (x : Matrix l m α) => x * M, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.addMonoidHomMulRight_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix m n α) (x : Matrix l m α) : M.addMonoidHomMulRight x = x * M

theorem Matrix.sum_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [NonUnitalNonAssocSemiring α] [Fintype m] (s : Finset β) (f : β → Matrix l m α) (M : Matrix m n α) : (∑ a ∈ s, f a) * M = ∑ a ∈ s, f a * M

theorem Matrix.mul_sum {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [NonUnitalNonAssocSemiring α] [Fintype m] (s : Finset β) (f : β → Matrix m n α) (M : Matrix l m α) : M * ∑ a ∈ s, f a = ∑ a ∈ s, M * f a

instance Matrix.Semiring.isScalarTower {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] : IsScalarTower R (Matrix n n α) (Matrix n n α)

This instance enables use with smul_mul_assoc.

instance Matrix.Semiring.smulCommClass {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α] : SMulCommClass R (Matrix n n α) (Matrix n n α)

This instance enables use with mul_smul_comm.

@[simp]

theorem Matrix.one_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (M : Matrix m n α) : 1 * M = M

@[simp]

theorem Matrix.mul_one {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] [DecidableEq n] (M : Matrix m n α) : M * 1 = M

instance Matrix.nonAssocSemiring {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] [DecidableEq n] : NonAssocSemiring (Matrix n n α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.map_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [NonAssocSemiring α] [Fintype n] {L : Matrix m n α} {M : Matrix n o α} [NonAssocSemiring β] {f : α →+* β} : (L * M).map ⇑f = L.map ⇑f * M.map ⇑f

theorem Matrix.smul_one_eq_diagonal {m : Type u_2} {α : Type v} [NonAssocSemiring α] [DecidableEq m] (a : α) : a • 1 = diagonal fun (x : m) => a

theorem Matrix.op_smul_one_eq_diagonal {m : Type u_2} {α : Type v} [NonAssocSemiring α] [DecidableEq m] (a : α) : MulOpposite.op a • 1 = diagonal fun (x : m) => a

theorem Matrix.mul_assoc {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype m] [Fintype n] (L : Matrix l m α) (M : Matrix m n α) (N : Matrix n o α) : L * M * N = L * (M * N)

instance Matrix.nonUnitalSemiring {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] : NonUnitalSemiring (Matrix n n α)

Equations

• Matrix.nonUnitalSemiring = { toNonUnitalNonAssocSemiring := Matrix.nonUnitalNonAssocSemiring, mul_assoc := ⋯ }

instance Matrix.semiring {n : Type u_3} {α : Type v} [Semiring α] [Fintype n] [DecidableEq n] : Semiring (Matrix n n α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.neg_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) : -M * N = -(M * N)

@[simp]

theorem Matrix.mul_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) : M * -N = -(M * N)

theorem Matrix.sub_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M M' : Matrix m n α) (N : Matrix n o α) : (M - M') * N = M * N - M' * N

theorem Matrix.mul_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M : Matrix m n α) (N N' : Matrix n o α) : M * (N - N') = M * N - M * N'

instance Matrix.nonUnitalNonAssocRing {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] : NonUnitalNonAssocRing (Matrix n n α)

Equations

• One or more equations did not get rendered due to their size.

instance Matrix.instNonUnitalRing {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalRing α] : NonUnitalRing (Matrix n n α)

Equations

• One or more equations did not get rendered due to their size.

instance Matrix.instNonAssocRing {n : Type u_3} {α : Type v} [Fintype n] [DecidableEq n] [NonAssocRing α] : NonAssocRing (Matrix n n α)

Equations

• One or more equations did not get rendered due to their size.

instance Matrix.instRing {n : Type u_3} {α : Type v} [Fintype n] [DecidableEq n] [Ring α] : Ring (Matrix n n α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.mul_mul_left {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Semiring α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) : (of fun (i : m) (j : n) => a * M i j) * N = a • (M * N)

theorem Matrix.smul_eq_mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [CommSemiring α] [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) : a • M = M * diagonal fun (x : n) => a

@[simp]

theorem Matrix.mul_mul_right {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [CommSemiring α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) : (M * of fun (i : n) (j : o) => a * N i j) = a • (M * N)

def Matrix.vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] (w : m → α) (v : n → α) : Matrix m n α

For two vectors w and v, vecMulVec w v i j is defined to be w i * v j. Put another way, vecMulVec w v is exactly col w * row v.

Equations

• Matrix.vecMulVec w v = Matrix.of fun (x : m) (y : n) => w x * v y

theorem Matrix.vecMulVec_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] (w : m → α) (v : n → α) (i : m) (j : n) : vecMulVec w v i j = w i * v j

def Matrix.mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (M : Matrix m n α) (v : n → α) : m → α

M *ᵥ v (notation for mulVec M v) is the matrix-vector product of matrix M and vector v, where v is seen as a column vector. Put another way, M *ᵥ v is the vector whose entries are those of M * col v (see col_mulVec).

The notation has precedence 73, which comes immediately before ⬝ᵥ for dotProduct, so that A *ᵥ v ⬝ᵥ B *ᵥ w is parsed as (A *ᵥ v) ⬝ᵥ (B *ᵥ w).

Equations

• M.mulVec v x✝ = (fun (j : n) => M x✝ j) ⬝ᵥ v

def Matrix.«term_*ᵥ_» : Lean.TrailingParserDescr

M *ᵥ v (notation for mulVec M v) is the matrix-vector product of matrix M and vector v, where v is seen as a column vector. Put another way, M *ᵥ v is the vector whose entries are those of M * col v (see col_mulVec).

The notation has precedence 73, which comes immediately before ⬝ᵥ for dotProduct, so that A *ᵥ v ⬝ᵥ B *ᵥ w is parsed as (A *ᵥ v) ⬝ᵥ (B *ᵥ w).

Equations

• Matrix.«term_*ᵥ_» = Lean.ParserDescr.trailingNode `Matrix.«term_*ᵥ_» 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *ᵥ ") (Lean.ParserDescr.cat `term 73))

def Matrix.vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (v : m → α) (M : Matrix m n α) : n → α

v ᵥ* M (notation for vecMul v M) is the vector-matrix product of vector v and matrix M, where v is seen as a row vector. Put another way, v ᵥ* M is the vector whose entries are those of row v * M (see row_vecMul).

The notation has precedence 73, which comes immediately before ⬝ᵥ for dotProduct, so that v ᵥ* A ⬝ᵥ w ᵥ* B is parsed as (v ᵥ* A) ⬝ᵥ (w ᵥ* B).

Equations

• Matrix.vecMul v M x✝ = v ⬝ᵥ fun (i : m) => M i x✝

def Matrix.«term_ᵥ*_» : Lean.TrailingParserDescr

v ᵥ* M (notation for vecMul v M) is the vector-matrix product of vector v and matrix M, where v is seen as a row vector. Put another way, v ᵥ* M is the vector whose entries are those of row v * M (see row_vecMul).

The notation has precedence 73, which comes immediately before ⬝ᵥ for dotProduct, so that v ᵥ* A ⬝ᵥ w ᵥ* B is parsed as (v ᵥ* A) ⬝ᵥ (w ᵥ* B).

Equations

• Matrix.«term_ᵥ*_» = Lean.ParserDescr.trailingNode `Matrix.«term_ᵥ*_» 73 73 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᵥ* ") (Lean.ParserDescr.cat `term 74))

def Matrix.mulVec.addMonoidHomLeft {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : n → α) : Matrix m n α →+ m → α

Left multiplication by a matrix, as an AddMonoidHom from vectors to vectors.

Equations

• Matrix.mulVec.addMonoidHomLeft v = { toFun := fun (M : Matrix m n α) => M.mulVec v, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Matrix.mulVec.addMonoidHomLeft_apply {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : n → α) (M : Matrix m n α) (a✝ : m) : (addMonoidHomLeft v) M a✝ = M.mulVec v a✝

theorem Matrix.mul_apply_eq_vecMul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A : Matrix m n α) (B : Matrix n o α) (i : m) : (A * B) i = vecMul (A i) B

The ith row of the multiplication is the same as the vecMul with the ith row of A.

theorem Matrix.vecMul_eq_sum {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (v : m → α) (M : Matrix m n α) : vecMul v M = ∑ i : m, v i • M i

theorem Matrix.mulVec_eq_sum {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : n → α) (M : Matrix m n α) : M.mulVec v = ∑ i : n, MulOpposite.op (v i) • M.transpose i

theorem Matrix.mulVec_diagonal {m : Type u_2} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (v w : m → α) (x : m) : (diagonal v).mulVec w x = v x * w x

theorem Matrix.vecMul_diagonal {m : Type u_2} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (v w : m → α) (x : m) : vecMul v (diagonal w) x = v x * w x

theorem Matrix.dotProduct_mulVec {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype n] [Fintype m] [NonUnitalSemiring R] (v : m → R) (A : Matrix m n R) (w : n → R) : v ⬝ᵥ A.mulVec w = vecMul v A ⬝ᵥ w

Associate the dot product of mulVec to the left.

@[simp]

theorem Matrix.mulVec_zero {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A : Matrix m n α) : A.mulVec 0 = 0

@[simp]

theorem Matrix.zero_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (A : Matrix m n α) : vecMul 0 A = 0

@[simp]

theorem Matrix.zero_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : n → α) : mulVec 0 v = 0

@[simp]

theorem Matrix.vecMul_zero {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (v : m → α) : vecMul v 0 = 0

theorem Matrix.smul_mulVec_assoc {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] (a : R) (A : Matrix m n α) (b : n → α) : (a • A).mulVec b = a • A.mulVec b

theorem Matrix.mulVec_add {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A : Matrix m n α) (x y : n → α) : A.mulVec (x + y) = A.mulVec x + A.mulVec y

theorem Matrix.add_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A B : Matrix m n α) (x : n → α) : (A + B).mulVec x = A.mulVec x + B.mulVec x

theorem Matrix.vecMul_add {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (A B : Matrix m n α) (x : m → α) : vecMul x (A + B) = vecMul x A + vecMul x B

theorem Matrix.add_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (A : Matrix m n α) (x y : m → α) : vecMul (x + y) A = vecMul x A + vecMul y A

theorem Matrix.vecMul_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonUnitalNonAssocSemiring S] [DistribSMul R S] [IsScalarTower R S S] (M : Matrix n m S) (b : R) (v : n → S) : vecMul (b • v) M = b • vecMul v M

theorem Matrix.mulVec_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonUnitalNonAssocSemiring S] [DistribSMul R S] [SMulCommClass R S S] (M : Matrix m n S) (b : R) (v : n → S) : M.mulVec (b • v) = b • M.mulVec v

@[simp]

theorem Matrix.mulVec_single {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (M : Matrix m n R) (j : n) (x : R) : M.mulVec (Pi.single j x) = MulOpposite.op x • M.col j

@[simp]

theorem Matrix.single_vecMul {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring R] (M : Matrix m n R) (i : m) (x : R) : vecMul (Pi.single i x) M = x • M.row i

theorem Matrix.mulVec_single_one {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonAssocSemiring R] (M : Matrix m n R) (j : n) : M.mulVec (Pi.single j 1) = M.col j

theorem Matrix.single_one_vecMul {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype m] [DecidableEq m] [NonAssocSemiring R] (i : m) (M : Matrix m n R) : vecMul (Pi.single i 1) M = M.row i

theorem Matrix.diagonal_mulVec_single {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R) (j : n) (x : R) : (diagonal v).mulVec (Pi.single j x) = Pi.single j (v j * x)

theorem Matrix.single_vecMul_diagonal {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R) (j : n) (x : R) : vecMul (Pi.single j x) (diagonal v) = Pi.single j (x * v j)

@[simp]

theorem Matrix.vecMul_vecMul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype n] [Fintype m] (v : m → α) (M : Matrix m n α) (N : Matrix n o α) : vecMul (vecMul v M) N = vecMul v (M * N)

@[simp]

theorem Matrix.mulVec_mulVec {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype n] [Fintype o] (v : o → α) (M : Matrix m n α) (N : Matrix n o α) : M.mulVec (N.mulVec v) = (M * N).mulVec v

theorem Matrix.mul_mul_apply {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] (A B C : Matrix n n α) (i j : n) : (A * B * C) i j = A i ⬝ᵥ B.mulVec (C.transpose j)

theorem Matrix.mulVec_one {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] (A : Matrix m n α) : A.mulVec 1 = ∑ j : n, A.transpose j

theorem Matrix.one_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] (A : Matrix m n α) : vecMul 1 A = ∑ i : m, A i

@[deprecated Matrix.one_vecMul (since := "2025-01-26")]

theorem Matrix.vec_one_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] (A : Matrix m n α) : vecMul 1 A = ∑ i : m, A i

Alias of Matrix.one_vecMul.

theorem Matrix.ext_of_mulVec_single {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [DecidableEq n] [Fintype n] {M N : Matrix m n α} (h : ∀ (i : n), M.mulVec (Pi.single i 1) = N.mulVec (Pi.single i 1)) : M = N

theorem Matrix.ext_of_single_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [DecidableEq m] [Fintype m] {M N : Matrix m n α} (h : ∀ (i : m), vecMul (Pi.single i 1) M = vecMul (Pi.single i 1) N) : M = N

@[simp]

theorem Matrix.one_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (v : m → α) : mulVec 1 v = v

@[simp]

theorem Matrix.vecMul_one {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (v : m → α) : vecMul v 1 = v

@[simp]

theorem Matrix.diagonal_const_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : α) (v : m → α) : (diagonal fun (x_1 : m) => x).mulVec v = x • v

@[simp]

theorem Matrix.vecMul_diagonal_const {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : α) (v : m → α) : vecMul v (diagonal fun (x_1 : m) => x) = MulOpposite.op x • v

@[simp]

theorem Matrix.natCast_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ℕ) (v : m → α) : (↑x).mulVec v = ↑x • v

@[simp]

theorem Matrix.vecMul_natCast {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ℕ) (v : m → α) : vecMul v ↑x = MulOpposite.op ↑x • v

@[simp]

theorem Matrix.ofNat_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ℕ) [x.AtLeastTwo] (v : m → α) : (OfNat.ofNat x).mulVec v = OfNat.ofNat x • v

@[simp]

theorem Matrix.vecMul_ofNat {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ℕ) [x.AtLeastTwo] (v : m → α) : vecMul v (OfNat.ofNat x) = MulOpposite.op (OfNat.ofNat x) • v

theorem Matrix.neg_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (v : m → α) (A : Matrix m n α) : vecMul (-v) A = -vecMul v A

theorem Matrix.vecMul_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (v : m → α) (A : Matrix m n α) : vecMul v (-A) = -vecMul v A

theorem Matrix.neg_vecMul_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (v : m → α) (A : Matrix m n α) : vecMul (-v) (-A) = vecMul v A

theorem Matrix.neg_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (v : n → α) (A : Matrix m n α) : (-A).mulVec v = -A.mulVec v

theorem Matrix.mulVec_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (v : n → α) (A : Matrix m n α) : A.mulVec (-v) = -A.mulVec v

theorem Matrix.neg_mulVec_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (v : n → α) (A : Matrix m n α) : (-A).mulVec (-v) = A.mulVec v

theorem Matrix.mulVec_sub {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (A : Matrix m n α) (x y : n → α) : A.mulVec (x - y) = A.mulVec x - A.mulVec y

theorem Matrix.sub_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (A B : Matrix m n α) (x : n → α) : (A - B).mulVec x = A.mulVec x - B.mulVec x

theorem Matrix.vecMul_sub {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (A B : Matrix m n α) (x : m → α) : vecMul x (A - B) = vecMul x A - vecMul x B

theorem Matrix.sub_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (A : Matrix m n α) (x y : m → α) : vecMul (x - y) A = vecMul x A - vecMul y A

theorem Matrix.mulVec_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalCommSemiring α] [Fintype m] (A : Matrix m n α) (x : m → α) : A.transpose.mulVec x = vecMul x A

theorem Matrix.vecMul_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalCommSemiring α] [Fintype n] (A : Matrix m n α) (x : n → α) : vecMul x A.transpose = A.mulVec x

theorem Matrix.mulVec_vecMul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalCommSemiring α] [Fintype n] [Fintype o] (A : Matrix m n α) (B : Matrix o n α) (x : o → α) : A.mulVec (vecMul x B) = (A * B.transpose).mulVec x

theorem Matrix.vecMul_mulVec {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalCommSemiring α] [Fintype m] [Fintype n] (A : Matrix m n α) (B : Matrix m o α) (x : n → α) : vecMul (A.mulVec x) B = vecMul x (A.transpose * B)

theorem Matrix.mulVec_injective_of_isUnit {m : Type u_2} {R : Type u_7} [Semiring R] [Fintype m] [DecidableEq m] {A : Matrix m m R} (ha : IsUnit A) : Function.Injective A.mulVec

theorem Matrix.vecMul_injective_of_isUnit {m : Type u_2} {R : Type u_7} [Semiring R] [Fintype m] [DecidableEq m] {A : Matrix m m R} (ha : IsUnit A) : Function.Injective fun (v : m → R) => vecMul v A

theorem Matrix.mulVec_smul_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [CommSemiring α] [Fintype n] (A : Matrix m n α) (b : n → α) (a : α) : A.mulVec (a • b) = a • A.mulVec b

@[simp]

theorem Matrix.intCast_mulVec {m : Type u_2} {α : Type v} [NonAssocRing α] [Fintype m] [DecidableEq m] (x : ℤ) (v : m → α) : (↑x).mulVec v = ↑x • v

@[simp]

theorem Matrix.vecMul_intCast {m : Type u_2} {α : Type v} [NonAssocRing α] [Fintype m] [DecidableEq m] (x : ℤ) (v : m → α) : vecMul v ↑x = MulOpposite.op ↑x • v

@[simp]

theorem Matrix.transpose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommMonoid α] [CommMagma α] [Fintype n] (M : Matrix m n α) (N : Matrix n l α) : (M * N).transpose = N.transpose * M.transpose

theorem Matrix.submatrix_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type u_10} {q : Type u_11} (M : Matrix m n α) (N : Matrix n p α) (e₁ : l → m) (e₂ : o → n) (e₃ : q → p) (he₂ : Function.Bijective e₂) : (M * N).submatrix e₁ e₃ = M.submatrix e₁ e₂ * N.submatrix e₂ e₃

simp lemmas for Matrix.submatrixs interaction with Matrix.diagonal, 1, and Matrix.mul for when the mappings are bundled.

@[simp]

theorem Matrix.submatrix_mul_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [AddCommMonoid α] [Mul α] {p : Type u_10} {q : Type u_11} (M : Matrix m n α) (N : Matrix n p α) (e₁ : l → m) (e₂ : o ≃ n) (e₃ : q → p) : M.submatrix e₁ ⇑e₂ * N.submatrix (⇑e₂) e₃ = (M * N).submatrix e₁ e₃

theorem Matrix.submatrix_mulVec_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : o → α) (e₁ : l → m) (e₂ : o ≃ n) : (M.submatrix e₁ ⇑e₂).mulVec v = M.mulVec (v ∘ ⇑e₂.symm) ∘ e₁

@[simp]

theorem Matrix.submatrix_id_mul_left {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type u_10} (M : Matrix m n α) (N : Matrix o p α) (e₁ : l → m) (e₂ : n ≃ o) : M.submatrix e₁ id * N.submatrix (⇑e₂) id = M.submatrix e₁ ⇑e₂.symm * N

@[simp]

theorem Matrix.submatrix_id_mul_right {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type u_10} (M : Matrix m n α) (N : Matrix o p α) (e₁ : l → p) (e₂ : o ≃ n) : M.submatrix id ⇑e₂ * N.submatrix id e₁ = M * N.submatrix (⇑e₂.symm) e₁

theorem Matrix.submatrix_vecMul_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : l → α) (e₁ : l ≃ m) (e₂ : o → n) : vecMul v (M.submatrix (⇑e₁) e₂) = vecMul (v ∘ ⇑e₁.symm) M ∘ e₂

theorem Matrix.mul_submatrix_one {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : n ≃ o) (e₂ : l → o) (M : Matrix m n α) : M * submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)

theorem Matrix.one_submatrix_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype m] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : l → o) (e₂ : m ≃ o) (M : Matrix m n α) : submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id

theorem Matrix.submatrix_mul_transpose_submatrix {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [AddCommMonoid α] [Mul α] (e : m ≃ n) (M : Matrix m n α) : M.submatrix id ⇑e * M.transpose.submatrix (⇑e) id = M * M.transpose

theorem RingHom.map_matrix_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [Fintype n] [NonAssocSemiring α] [NonAssocSemiring β] (M : Matrix m n α) (N : Matrix n o α) (i : m) (j : o) (f : α →+* β) : f ((M * N) i j) = (M.map ⇑f * N.map ⇑f) i j

theorem RingHom.map_dotProduct {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (v w : n → R) : f (v ⬝ᵥ w) = ⇑f ∘ v ⬝ᵥ ⇑f ∘ w

theorem RingHom.map_vecMul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix n m R) (v : n → R) (i : m) : f (Matrix.vecMul v M i) = Matrix.vecMul (⇑f ∘ v) (M.map ⇑f) i

theorem RingHom.map_mulVec {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix m n R) (v : n → R) (i : m) : f (M.mulVec v i) = (M.map ⇑f).mulVec (⇑f ∘ v) i