HepLean Documentation

Mathlib.Data.Matrix.Mul

Matrix multiplication #

This file defines matrix multiplication

Main definitions #

Matrix.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 Matrix.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 Matrix.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

Matrix.dotProduct v w = ∑ i : m, v i * w i

Instances For

def Matrix.«term_⬝ᵥ_» :

Lean.TrailingParserDescr

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

Equations

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

Instances For

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 α) :

Matrix.dotProduct (fun (j : n) => Matrix.dotProduct u fun (i : m) => v i j) w = Matrix.dotProduct u fun (i : m) => Matrix.dotProduct (v i) w

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

Matrix.dotProduct v w = Matrix.dotProduct w v

@[simp]

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

Matrix.dotProduct v w = v PUnit.unit * w PUnit.unit

theorem Matrix.dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : n → α) :

Matrix.dotProduct v 1 = ∑ i : n, v i

theorem Matrix.one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : n → α) :

Matrix.dotProduct 1 v = ∑ i : n, v i

@[simp]

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

Matrix.dotProduct v 0 = 0

@[simp]

theorem Matrix.dotProduct_zero' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) :

(Matrix.dotProduct v fun (x : m) => 0) = 0

@[simp]

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

Matrix.dotProduct 0 v = 0

@[simp]

theorem Matrix.zero_dotProduct' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) :

Matrix.dotProduct (fun (x : m) => 0) v = 0

@[simp]

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

Matrix.dotProduct (u + v) w = Matrix.dotProduct u w + Matrix.dotProduct v w

@[simp]

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

Matrix.dotProduct u (v + w) = Matrix.dotProduct u v + Matrix.dotProduct u w

@[simp]

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 → α) :

Matrix.dotProduct (Sum.elim u x) (Sum.elim v y) = Matrix.dotProduct u v + Matrix.dotProduct x y

@[simp]

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) :

Matrix.dotProduct (u ∘ ⇑e.symm) x = Matrix.dotProduct u (x ∘ ⇑e)

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

@[simp]

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) :

Matrix.dotProduct u (x ∘ ⇑e.symm) = Matrix.dotProduct (u ∘ ⇑e) x

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

@[simp]

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) :

Matrix.dotProduct (x ∘ ⇑e) (y ∘ ⇑e) = Matrix.dotProduct x y

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

@[simp]

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

Matrix.dotProduct (Matrix.diagonal v i) w = v i * w i

@[simp]

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

Matrix.dotProduct v (Matrix.diagonal w i) = v i * w i

@[simp]

theorem Matrix.dotProduct_diagonal' {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : m → α) (i : m) :

(Matrix.dotProduct v fun (j : m) => Matrix.diagonal w j i) = v i * w i

@[simp]

theorem Matrix.single_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (x : α) (i : m) :

Matrix.dotProduct (Pi.single i x) v = x * v i

@[simp]

theorem Matrix.dotProduct_single {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : m → α) (x : α) (i : m) :

Matrix.dotProduct v (Pi.single i x) = v i * x

@[simp]

theorem Matrix.one_dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] :

Matrix.dotProduct 1 1 = ↑(Fintype.card n)

theorem Matrix.dotProduct_single_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] [DecidableEq n] (v : n → α) (i : n) :

Matrix.dotProduct v (Pi.single i 1) = v i

theorem Matrix.single_one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] [DecidableEq n] (i : n) (v : n → α) :

Matrix.dotProduct (Pi.single i 1) v = v i

@[simp]

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

Matrix.dotProduct (-v) w = -Matrix.dotProduct v w

@[simp]

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

Matrix.dotProduct v (-w) = -Matrix.dotProduct v w

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

Matrix.dotProduct (-v) (-w) = Matrix.dotProduct v w

@[simp]

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

Matrix.dotProduct (u - v) w = Matrix.dotProduct u w - Matrix.dotProduct v w

@[simp]

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

Matrix.dotProduct u (v - w) = Matrix.dotProduct u v - Matrix.dotProduct u w

@[simp]

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 → α) :

Matrix.dotProduct (x • v) w = x • Matrix.dotProduct v w

@[simp]

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 → α) :

Matrix.dotProduct v (x • w) = x • Matrix.dotProduct v w

@[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) => Matrix.dotProduct (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 = Matrix.dotProduct (fun (j : m) => M i j) fun (j : m) => N j k

theorem Matrix.two_mul_expl {R : Type u_10} [CommRing 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

Matrix.nonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

@[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) :

(Matrix.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 * Matrix.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 → α) :

Matrix.diagonal d₁ * Matrix.diagonal d₂ = Matrix.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 → α) :

Matrix.diagonal d₁ * Matrix.diagonal d₂ = Matrix.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 = (Matrix.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 * Matrix.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' := ⋯ }

Instances For

@[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' := ⋯ }

Instances For

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

Equations

⋯ = ⋯

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.

Equations

⋯ = ⋯

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

Matrix.nonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

@[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 = Matrix.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 = Matrix.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 = NonUnitalSemiring.mk ⋯

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

Semiring (Matrix n n α)

Equations

Matrix.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯

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

Matrix.nonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

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

NonUnitalRing (Matrix n n α)

Equations

Matrix.instNonUnitalRing = NonUnitalRing.mk ⋯

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

NonAssocRing (Matrix n n α)

Equations

Matrix.instNonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Ring (Matrix n n α)

Equations

Matrix.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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 : α) :

(Matrix.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 * Matrix.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 * Matrix.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

Instances For

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

Matrix.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 Matrix.dotProduct, so that A *ᵥ v ⬝ᵥ B *ᵥ w is parsed as (A *ᵥ v) ⬝ᵥ (B *ᵥ w).

Equations

M.mulVec v x = Matrix.dotProduct (fun (j : n) => M x j) v

Instances For

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 Matrix.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))

Instances For

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 Matrix.dotProduct, so that v ᵥ* A ⬝ᵥ w ᵥ* B is parsed as (v ᵥ* A) ⬝ᵥ (w ᵥ* B).

Equations

Matrix.vecMul v M x = Matrix.dotProduct v fun (i : m) => M i x

Instances For

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 Matrix.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))

Instances For

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' := ⋯ }

Instances For

@[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) :

(Matrix.mulVec.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 = Matrix.vecMul (A i) B

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

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

(Matrix.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) :

Matrix.vecMul v (Matrix.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) :

Matrix.dotProduct v (A.mulVec w) = Matrix.dotProduct (Matrix.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 α) :

Matrix.vecMul 0 A = 0

@[simp]

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

Matrix.mulVec 0 v = 0

@[simp]

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

Matrix.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 → α) :

Matrix.vecMul x (A + B) = Matrix.vecMul x A + Matrix.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 → α) :

Matrix.vecMul (x + y) A = Matrix.vecMul x A + Matrix.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] [Monoid R] [NonUnitalNonAssocSemiring S] [DistribMulAction R S] [IsScalarTower R S S] (M : Matrix n m S) (b : R) (v : n → S) :

Matrix.vecMul (b • v) M = b • Matrix.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] [Monoid R] [NonUnitalNonAssocSemiring S] [DistribMulAction 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) = fun (i : m) => M i j * x

@[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) :

Matrix.vecMul (Pi.single i x) M = fun (j : n) => x * M i j

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.transpose 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) :

Matrix.vecMul (Pi.single i 1) M = M 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) :

(Matrix.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) :

Matrix.vecMul (Pi.single j x) (Matrix.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 α) :

Matrix.vecMul (Matrix.vecMul v M) N = Matrix.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 = Matrix.dotProduct (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 = fun (i : m) => ∑ j : n, A i j

theorem Matrix.vec_one_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] (A : Matrix m n α) :

Matrix.vecMul 1 A = fun (j : n) => ∑ i : m, A i j

@[simp]

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

Matrix.mulVec 1 v = v

@[simp]

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

Matrix.vecMul v 1 = v

@[simp]

theorem Matrix.diagonal_const_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : α) (v : m → α) :

(Matrix.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 → α) :

Matrix.vecMul v (Matrix.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 → α) :

Matrix.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 → α) :

Matrix.mulVec (OfNat.ofNat x) 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 → α) :

Matrix.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 α) :

Matrix.vecMul (-v) A = -Matrix.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 α) :

Matrix.vecMul v (-A) = -Matrix.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 α) :

Matrix.vecMul (-v) (-A) = Matrix.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 → α) :

Matrix.vecMul x (A - B) = Matrix.vecMul x A - Matrix.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 → α) :

Matrix.vecMul (x - y) A = Matrix.vecMul x A - Matrix.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 = Matrix.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 → α) :

Matrix.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 (Matrix.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 → α) :

Matrix.vecMul (A.mulVec x) B = Matrix.vecMul x (A.transpose * B)

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 → α) :

Matrix.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 α] [CommSemigroup α] [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) :

Matrix.vecMul v (M.submatrix (⇑e₁) e₂) = Matrix.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 * Matrix.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 α) :

Matrix.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 (Matrix.dotProduct v w) = Matrix.dotProduct (⇑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