Documentation

Mathlib.Data.Matrix.Mul

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.

Equations

Instances For

def «term_⬝ᵥ_» :

Lean.TrailingParserDescr

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

See also dotProductEquiv.

Equations

Instances For

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

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

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

instance Matrix.instMulOneOfFintypeOfDecidableEqOfAddCommMonoid {n : Type u_3} {α : Type v} [Fintype n] [DecidableEq n] [MulOne α] [AddCommMonoid α] :

MulOne (Matrix n n α)

Equations

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

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

NonUnitalNonAssocSemiring (Matrix n n α)

Equations

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

Equations

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

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.

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

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

NonAssocSemiring (Matrix n n α)

Equations

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

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

Semiring (Matrix n n α)

Equations

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

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

NonUnitalRing (Matrix n n α)

Equations

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

NonAssocRing (Matrix n n α)

Equations

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

Ring (Matrix n n α)

Equations

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

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

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

Instances

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.

Equations

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

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

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

Equations

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

Equations

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

Equations

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

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

(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