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

source
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

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

Instances For

source
def «term_⬝ᵥ_» :
Lean.TrailingParserDescr

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

See also `dotProductEquiv`.

Equations

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

Instances For

source
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
source
theorem dotProduct_comm {m : Type u_2} {α : Type v} [Fintype m] [AddCommMonoid α] [CommMagma α] (v w : m → α) :
v ⬝ᵥ w = w ⬝ᵥ v
source
@[simp]
theorem dotProduct_pUnit {α : Type v} [AddCommMonoid α] [Mul α] (v w : PUnit.{u_10 + 1} → α) :
v ⬝ᵥ w = v PUnit.unit * w PUnit.unit
source
theorem dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : n → α) :
v ⬝ᵥ 1 = ∑ i : n, v i
source
theorem one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : n → α) :
1 ⬝ᵥ v = ∑ i : n, v i
source
@[simp]
theorem dotProduct_zero {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) :
v ⬝ᵥ 0 = 0
source
@[simp]
theorem dotProduct_zero' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) :
(v ⬝ᵥ fun (x : m) => 0) = 0
source
@[simp]
theorem zero_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) :
0 ⬝ᵥ v = 0
source
@[simp]
theorem zero_dotProduct' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : m → α) :
(fun (x : m) => 0) ⬝ᵥ v = 0
source
@[simp]
theorem add_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u v w : m → α) :
(u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w
source
@[simp]
theorem dotProduct_add {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u v w : m → α) :
u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w
source
@[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
source
@[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.

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

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

source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem one_dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] :
1 ⬝ᵥ 1 = ↑(Fintype.card n)
source
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
source
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
source
@[simp]
theorem neg_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : m → α) :
-v ⬝ᵥ w = -(v ⬝ᵥ w)
source
@[simp]
theorem dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : m → α) :
v ⬝ᵥ -w = -(v ⬝ᵥ w)
source
theorem neg_dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : m → α) :
-v ⬝ᵥ -w = v ⬝ᵥ w
source
@[simp]
theorem sub_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u v w : m → α) :
(u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w
source
@[simp]
theorem dotProduct_sub {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u v w : m → α) :
u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w
source
@[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)
source
@[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)
source
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.

source
theorem not_injective_dotProduct_left {m : Type u_2} {α : Type v} [Fintype m] [CommRing α] [Nontrivial m] [Nontrivial α] (a : m → α) :
¬Function.Injective (dotProduct a)
source
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
source
@[defaultInstance 100]
instance Matrix.instHMulOfFintypeOfMulOfAddCommMonoid {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] :
HMul (Matrix l m α) (Matrix m n α) (Matrix l n α)

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

Equations

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

source
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
source
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 }

source
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
source
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
source
@[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)
source
@[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)
source
@[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
source
@[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
source
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
source
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
source
instance Matrix.nonUnitalNonAssocSemiring {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] :
NonUnitalNonAssocSemiring (Matrix n n α)
Equations

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

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

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

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

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

source
@[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
source
@[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
source
instance Matrix.nonAssocSemiring {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] [DecidableEq n] :
NonAssocSemiring (Matrix n n α)
Equations

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

source
@[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
source
theorem Matrix.smul_one_eq_diagonal {m : Type u_2} {α : Type v} [NonAssocSemiring α] [DecidableEq m] (a : α) :
a • 1 = diagonal fun (x : m) => a
source
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
source
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)
source
instance Matrix.nonUnitalSemiring {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] :
NonUnitalSemiring (Matrix n n α)
Equations

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

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

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

source
@[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)
source
@[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)
source
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
source
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'
source
instance Matrix.nonUnitalNonAssocRing {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] :
NonUnitalNonAssocRing (Matrix n n α)
Equations

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

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

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

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

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

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

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

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

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

Instances For

source
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
source
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
source
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
source
@[simp]
theorem Matrix.zero_vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [MulZeroClass α] (v : n → α) :
vecMulVec 0 v = 0
source
@[simp]
theorem Matrix.vecMulVec_zero {m : Type u_2} {α : Type v} [MulZeroClass α] (w : m → α) :
vecMulVec w 0 = 0
source
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
source
@[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
source
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
source
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₂
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
@[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
source
@[simp]
theorem Matrix.diag_vecMulVec {n : Type u_3} {α : Type v} [Mul α] (u v : n → α) :
(vecMulVec u v).diag = u * v
source
def Matrix.mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (M : Matrix m n α) (v : n → α) :
m → α

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

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

Equations

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

Instances For

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

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

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

Equations

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

Instances For

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

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

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

Equations

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

Instances For

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

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

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

Equations

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

Instances For

source
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

source
@[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✝
source
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 `i`th row of the multiplication is the same as the `vecMul` with the `i`th row of `A`.

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

source
@[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
source
@[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
source
@[simp]
theorem Matrix.zero_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : n → α) :
mulVec 0 v = 0
source
@[simp]
theorem Matrix.vecMul_zero {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (v : m → α) :
vecMul v 0 = 0
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[deprecated Matrix.smul_mulVec (since := "2025-08-14")]
theorem Matrix.smul_mulVec_assoc {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

Alias of `Matrix.smul_mulVec`.

source
@[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
source
@[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
source
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
source
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
source
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)
source
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)
source
@[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)
source
@[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
source
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)
source
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
source
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
source
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
source
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)
source
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)
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem Matrix.mulVec_injective {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] :
Function.Injective mulVec
source
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
source
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
source
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
source
@[simp]
theorem Matrix.one_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (v : m → α) :
mulVec 1 v = v
source
@[simp]
theorem Matrix.vecMul_one {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (v : m → α) :
vecMul v 1 = v
source
@[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
source
@[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
source
@[simp]
theorem Matrix.natCast_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ℕ) (v : m → α) :
(↑x).mulVec v = ↑x • v
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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₂
source
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
source
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
source
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
source
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)
source
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
source
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
source
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
source
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
source
@[deprecated Matrix.mulVec_smul (since := "2025-08-14")]
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
source
@[simp]
theorem Matrix.intCast_mulVec {m : Type u_2} {α : Type v} [NonAssocRing α] [Fintype m] [DecidableEq m] (x : ℤ) (v : m → α) :
(↑x).mulVec v = ↑x • v
source
@[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
source
@[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
source
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.submatrix`s interaction with `Matrix.diagonal`, `1`, and `Matrix.mul` for when the mappings are bundled.

source
@[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₃
source
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₁
source
@[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
source
@[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₁
source
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₂
source
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₂)
source
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
source
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
source
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
source
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
source
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
source
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