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 scope Matrix gives the following notation:

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

See Mathlib/LinearAlgebra/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.

See also dotProductEquiv.

def «term_⬝ᵥ_» : Lean.TrailingParserDescr

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

See also dotProductEquiv.

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem dotProduct_sum {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] {ι : Type u_10} (u : m → α) (s : Finset ι) (v : ι → m → α) : u ⬝ᵥ ∑ i ∈ s, v i = ∑ i ∈ s, u ⬝ᵥ v i

theorem sum_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] {ι : Type u_10} (s : Finset ι) (u : ι → m → α) (v : m → α) : (∑ i ∈ s, u i) ⬝ᵥ v = ∑ i ∈ s, u i ⬝ᵥ v

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem exists_ne_zero_dotProduct_eq_zero {m : Type u_2} {α : Type v} [Fintype m] [CommRing α] [Nontrivial m] [Nontrivial α] (a : m → α) : ∃ (b : m → α), b ≠ 0 ∧ b ⬝ᵥ a = 0

For any vector a in a nontrivial commutative ring with nontrivial index, there exists a non-zero vector b such that b ⬝ᵥ a = 0. In other words, there exists a non-zero orthogonal vector.

theorem not_injective_dotProduct_left {m : Type u_2} {α : Type v} [Fintype m] [CommRing α] [Nontrivial m] [Nontrivial α] (a : m → α) : ¬Function.Injective (dotProduct a)

theorem not_injective_dotProduct_right {m : Type u_2} {α : Type v} [Fintype m] [CommRing α] [Nontrivial m] [Nontrivial α] (a : m → α) : ¬Function.Injective fun (x : m → α) => x ⬝ᵥ a

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

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Matrix.instMulOneOfFintypeOfDecidableEqOfAddCommMonoid {n : Type u_3} {α : Type v} [Fintype n] [DecidableEq n] [MulOne α] [AddCommMonoid α] : MulOne (Matrix n 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 = M i ⬝ᵥ 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

@[implicit_reducible]

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

@[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.commute_diagonal {n : Type u_3} {α : Type u_10} [NonUnitalNonAssocCommSemiring α] [Fintype n] [DecidableEq n] (d₁ d₂ : n → α) : Commute (diagonal d₁) (diagonal d₂)

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.

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

@[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.map_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [NonUnitalNonAssocSemiring α] [Fintype n] {L : Matrix m n α} {M : Matrix n o α} [NonUnitalNonAssocSemiring β] {F : Type u_10} [FunLike F α β] [NonUnitalRingHomClass F α β] {f : F} : (L * M).map ⇑f = L.map ⇑f * M.map ⇑f

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

@[implicit_reducible]

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

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)

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[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.pow_apply_nonneg {n : Type u_3} {α : Type v} [Semiring α] [Fintype n] [DecidableEq n] [PartialOrder α] [IsOrderedRing α] {A : Matrix n n α} (hA : ∀ (i j : n), 0 ≤ A i j) (k : ℕ) (i j : n) : 0 ≤ (A ^ k) i j

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)

class IsStablyFiniteRing (R : Type u_10) [MulOne R] [AddCommMonoid R] : Prop

A semiring is stably finite if every matrix ring over it is Dedekind-finite.

• isDedekindFiniteMonoid (n : ℕ) : IsDedekindFiniteMonoid (Matrix (Fin n) (Fin n) R)

theorem isStablyFiniteRing_iff (R : Type u_10) [MulOne R] [AddCommMonoid R] : IsStablyFiniteRing R ↔ ∀ (n : ℕ), IsDedekindFiniteMonoid (Matrix (Fin n) (Fin n) R)

@[instance 100]

instance instIsDedekindFiniteMonoidOfIsStablyFiniteRing (R : Type u_10) [NonAssocSemiring R] [IsStablyFiniteRing R] : IsDedekindFiniteMonoid R

theorem IsStablyFiniteRing.of_injective {R : Type u_10} {S : Type u_11} {F : Type u_12} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Injective ⇑f) [IsStablyFiniteRing S] : IsStablyFiniteRing R

theorem RingEquiv.isStablyFiniteRing_iff {R : Type u_10} {S : Type u_11} {F : Type u_12} [NonAssocSemiring R] [NonAssocSemiring S] [EquivLike F R S] [RingEquivClass F R S] (f : F) : IsStablyFiniteRing R ↔ IsStablyFiniteRing S

@[instance 100]

instance instIsStablyFiniteRingSubtypeMem {R : Type u_10} {F : Type u_12} [NonAssocSemiring R] [SetLike F R] [SubsemiringClass F R] (S : F) [IsStablyFiniteRing R] : IsStablyFiniteRing ↥S

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 replicateCol ι w * replicateRow ι v for Unique ι; see vecMulVec_eq.

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

theorem Matrix.row_vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] (w : m → α) (v : n → α) (i : m) : (vecMulVec w v).row i = w i • v

theorem Matrix.col_vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] (w : m → α) (v : n → α) (j : n) : (vecMulVec w v).col j = MulOpposite.op (v j) • w

@[simp]

theorem Matrix.zero_vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [MulZeroClass α] (v : n → α) : vecMulVec 0 v = 0

@[simp]

theorem Matrix.vecMulVec_zero {m : Type u_2} {α : Type v} [MulZeroClass α] (w : m → α) : vecMulVec w 0 = 0

theorem Matrix.vecMulVec_ne_zero {n : Type u_3} {α : Type v} [Mul α] [Zero α] [NoZeroDivisors α] {a b : n → α} (ha : a ≠ 0) (hb : b ≠ 0) : vecMulVec a b ≠ 0

@[simp]

theorem Matrix.vecMulVec_eq_zero {n : Type u_3} {α : Type v} [MulZeroClass α] [NoZeroDivisors α] {a b : n → α} : vecMulVec a b = 0 ↔ a = 0 ∨ b = 0

theorem Matrix.add_vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] [Add α] [RightDistribClass α] (w₁ w₂ : m → α) (v : n → α) : vecMulVec (w₁ + w₂) v = vecMulVec w₁ v + vecMulVec w₂ v

theorem Matrix.vecMulVec_add {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] [Add α] [LeftDistribClass α] (w : m → α) (v₁ v₂ : n → α) : vecMulVec w (v₁ + v₂) = vecMulVec w v₁ + vecMulVec w v₂

@[simp]

theorem Matrix.neg_vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] [HasDistribNeg α] (w : m → α) (v : n → α) : vecMulVec (-w) v = -vecMulVec w v

@[simp]

theorem Matrix.vecMulVec_neg {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] [HasDistribNeg α] (w : m → α) (v : n → α) : vecMulVec w (-v) = -vecMulVec w v

@[simp]

theorem Matrix.smul_vecMulVec {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Mul α] [SMul R α] [IsScalarTower R α α] (r : R) (w : m → α) (v : n → α) : vecMulVec (r • w) v = r • vecMulVec w v

@[simp]

theorem Matrix.vecMulVec_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [Mul α] [SMul R α] [SMulCommClass R α α] (r : R) (w : m → α) (v : n → α) : vecMulVec w (r • v) = r • vecMulVec w v

theorem Matrix.vecMulVec_smul' {m : Type u_2} {n : Type u_3} {α : Type v} [Semigroup α] (w : m → α) (r : α) (v : n → α) : vecMulVec w (r • v) = vecMulVec (MulOpposite.op r • w) v

@[simp]

theorem Matrix.transpose_vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [CommMagma α] (w : m → α) (v : n → α) : (vecMulVec w v).transpose = vecMulVec v w

@[simp]

theorem Matrix.diag_vecMulVec {n : Type u_3} {α : Type v} [Mul α] (u v : n → α) : (vecMulVec u v).diag = u * v

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.

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

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.

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

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.

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

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.

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

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.

@[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.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.mulVec_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DistribSMul R α] [SMulCommClass R α α] (M : Matrix m n α) (b : R) (v : n → α) : M.mulVec (b • v) = b • M.mulVec v

theorem Matrix.smul_mulVec {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DistribSMul R α] [IsScalarTower R α α] (b : R) (M : Matrix m n α) (v : n → α) : (b • M).mulVec v = b • M.mulVec v

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

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

@[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.vecMul_vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] (u v : m → α) (w : n → α) : vecMul u (vecMulVec v w) = (u ⬝ᵥ v) • w

theorem Matrix.vecMulVec_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] (u : m → α) (v w : n → α) : (vecMulVec u v).mulVec w = MulOpposite.op (v ⬝ᵥ w) • u

theorem Matrix.mul_vecMulVec {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] (M : Matrix l m α) (x : m → α) (y : n → α) : M * vecMulVec x y = vecMulVec (M.mulVec x) y

theorem Matrix.vecMulVec_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] (x : l → α) (y : m → α) (M : Matrix m n α) : vecMulVec x y * M = vecMulVec x (vecMul y M)

theorem Matrix.vecMulVec_mul_vecMulVec {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] (u : l → α) (v w : m → α) (x : n → α) : vecMulVec u v * vecMulVec w x = vecMulVec u ((v ⬝ᵥ w) • x)

theorem Matrix.mul_right_injective_iff_mulVec_injective {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype m] [Nonempty n] {A : Matrix l m α} : (Function.Injective fun (B : Matrix m n α) => A * B) ↔ Function.Injective A.mulVec

theorem Matrix.mul_left_injective_iff_vecMul_injective {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Nonempty l] [Fintype m] {A : Matrix m n α} : (Function.Injective fun (B : Matrix l m α) => B * A) ↔ Function.Injective fun (v : m → α) => vecMul v A

theorem Matrix.isLeftRegular_iff_mulVec_injective {m : Type u_2} {α : Type v} [NonUnitalSemiring α] [Fintype m] {A : Matrix m m α} : IsLeftRegular A ↔ Function.Injective A.mulVec

theorem Matrix.isRightRegular_iff_vecMul_injective {m : Type u_2} {α : Type v} [NonUnitalSemiring α] [Fintype m] {A : Matrix m m α} : IsRightRegular A ↔ Function.Injective fun (v : m → α) => vecMul v A

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

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

theorem Matrix.mulVec_injective {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] : Function.Injective mulVec

theorem Matrix.ext_iff_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] {A B : Matrix m n α} : A = B ↔ ∀ (v : n → α), A.mulVec v = B.mulVec v

theorem Matrix.vecMul_injective {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] : Function.Injective fun (x : Matrix m n α) (v : m → α) => vecMul v x

theorem Matrix.ext_iff_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] {A B : Matrix m n α} : A = B ↔ ∀ (v : m → α), vecMul v A = vecMul v B

@[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.sub_vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] (w₁ w₂ : m → α) (v : n → α) : vecMulVec (w₁ - w₂) v = vecMulVec w₁ v - vecMulVec w₂ v

theorem Matrix.vecMulVec_sub {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] (w : m → α) (v₁ v₂ : n → α) : vecMulVec w (v₁ - v₂) = vecMulVec w v₁ - vecMulVec w v₂

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.pow_row_eq_zero_of_le {n : Type u_3} {R : Type u_7} [Semiring R] [Fintype n] [DecidableEq n] {M : Matrix n n R} {k l : ℕ} {i : n} (h : (M ^ k).row i = 0) (h' : k ≤ l) : (M ^ l).row i = 0

theorem Matrix.pow_col_eq_zero_of_le {n : Type u_3} {R : Type u_7} [Semiring R] [Fintype n] [DecidableEq n] {M : Matrix n n R} {k l : ℕ} {i : n} (h : (M ^ k).col i = 0) (h' : k ≤ l) : (M ^ l).col i = 0

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

instance Matrix.instIsDedekindFiniteMonoidOfIsStablyFiniteRing (n : Type u_11) (R : Type u_12) [Fintype n] [DecidableEq n] [MulOne R] [AddCommMonoid R] [IsStablyFiniteRing R] : IsDedekindFiniteMonoid (Matrix n n R)

theorem Matrix.mul_eq_one_comm_of_equiv {m : Type u_10} {n : Type u_11} {R : Type u_12} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [MulOne R] [AddCommMonoid R] [IsStablyFiniteRing R] {A : Matrix m n R} {B : Matrix n m R} (e : m ≃ n) : A * B = 1 ↔ B * A = 1

A version of mul_eq_one_comm that works for square matrices with rectangular types.

theorem Matrix.mul_eq_one_comm_of_card_eq (m : Type u_10) (n : Type u_11) (R : Type u_12) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [MulOne R] [AddCommMonoid R] [IsStablyFiniteRing R] {A : Matrix m n R} {B : Matrix n m R} (eq : Fintype.card m = Fintype.card n) : A * B = 1 ↔ B * A = 1

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