Mathlib.Data.Matrix.Mul

dotProduct definition

[Mul α] [AddCommMonoid α] (v w : m → α) : α

Full source

/-- `dotProduct v w` is the sum of the entrywise products `v i * w i` -/
def dotProduct [Mul α] [AddCommMonoid α] (v w : m → α) : α :=
  ∑ i, v i * w i

Dot product of vectors

Informal description

Given an additive commutative monoid $\alpha$ with multiplication, the dot product of two vectors $v, w : m \to \alpha$ is defined as the sum $\sum_i v_i w_i$ of the entrywise products of their components.

term_⬝ᵥ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixl:72 " ⬝ᵥ " => dotProduct

Dot product notation

Informal description

The infix notation `⬝ᵥ` represents the dot product operation between two vectors. For vectors `v` and `w` of the same dimension with elements in a type `α` that has multiplication and forms an additive commutative monoid, `v ⬝ᵥ w` computes the sum of the products of corresponding elements: $\sum_{i} v_i w_i$.

dotProduct_assoc theorem

 [NonUnitalSemiring α] (u : m → α) (w : n → α) (v : Matrix m n α) :
  (fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w

Full source

theorem dotProduct_assoc [NonUnitalSemiring α] (u : m → α) (w : n → α) (v : Matrix m n α) :
    (fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w := by
  simpa [dotProduct, Finset.mul_sum, Finset.sum_mul, mul_assoc] using Finset.sum_comm

Associativity of Dot Product with Matrix Multiplication

Informal description

Let $\alpha$ be a non-unital semiring, $u : m \to \alpha$ and $w : n \to \alpha$ be vectors, and $v : \text{Matrix}\, m\, n\, \alpha$ be a matrix. Then the following equality holds: \[ \left(\sum_j u_j \left(\sum_i v_{ij}\right)\right) \cdot w_j = \sum_i u_i \left(\sum_j v_{ij} w_j\right). \]

dotProduct_comm theorem

[AddCommMonoid α] [CommMagma α] (v w : m → α) : v ⬝ᵥ w = w ⬝ᵥ v

Full source

theorem dotProduct_comm [AddCommMonoid α] [CommMagma α] (v w : m → α) : v ⬝ᵥ w = w ⬝ᵥ v := by
  simp_rw [dotProduct, mul_comm]

Commutativity of the Dot Product in a Commutative Monoid

Informal description

Let $\alpha$ be an additive commutative monoid with a commutative multiplication operation. For any two vectors $v, w : m \to \alpha$, their dot product satisfies $v \cdot w = w \cdot v$, where the dot product is defined as $\sum_i v_i w_i$.

dotProduct_pUnit theorem

[AddCommMonoid α] [Mul α] (v w : PUnit → α) : v ⬝ᵥ w = v ⟨⟩ * w ⟨⟩

Full source

@[simp]
theorem dotProduct_pUnit [AddCommMonoid α] [Mul α] (v w : PUnit → α) : v ⬝ᵥ w = v ⟨⟩ * w ⟨⟩ := by
  simp [dotProduct]

Dot Product on Singleton Type is Entrywise Product

Informal description

Let $\alpha$ be an additive commutative monoid with a multiplication operation. For any two vectors $v, w : \text{PUnit} \to \alpha$, their dot product equals the product of their single entries, i.e., \[ v \cdot w = v(\text{unit}) \cdot w(\text{unit}), \] where $\text{unit}$ is the unique element of $\text{PUnit}$.

dotProduct_one theorem

(v : n → α) : v ⬝ᵥ 1 = ∑ i, v i

Full source

theorem dotProduct_one (v : n → α) : v ⬝ᵥ 1 = ∑ i, v i := by simp [(· ⬝ᵥ ·)]

Dot Product with One Vector Yields Sum of Entries

Informal description

For any vector $v : n \to \alpha$ with entries in an additive commutative monoid $\alpha$ with multiplication, the dot product of $v$ with the constant one vector (where each entry is the multiplicative identity $1$) equals the sum of the entries of $v$, i.e., \[ v \cdot \mathbf{1} = \sum_{i} v_i. \]

one_dotProduct theorem

(v : n → α) : 1 ⬝ᵥ v = ∑ i, v i

Full source

theorem one_dotProduct (v : n → α) : 1 ⬝ᵥ v = ∑ i, v i := by simp [(· ⬝ᵥ ·)]

Dot Product with Constant One Vector Yields Sum of Entries

Informal description

For any vector $v : n \to \alpha$ with entries in an additive commutative monoid $\alpha$ with multiplication, the dot product of the constant vector $1$ (where every entry is the multiplicative identity) with $v$ equals the sum of the entries of $v$, i.e., $1 \cdot v = \sum_i v_i$.

dotProduct_zero theorem

: v ⬝ᵥ 0 = 0

Full source

@[simp]
theorem dotProduct_zero : v ⬝ᵥ 0 = 0 := by simp [dotProduct]

Dot Product with Zero Vector Yields Zero

Informal description

For any vector $v$ with entries in an additive commutative monoid $\alpha$ with multiplication, the dot product of $v$ with the zero vector equals the zero element of $\alpha$, i.e., $v \cdot 0 = 0$.

dotProduct_zero' theorem

: (v ⬝ᵥ fun _ => 0) = 0

Full source

@[simp]
theorem dotProduct_zero' : (v ⬝ᵥ fun _ => 0) = 0 :=
  dotProduct_zero v

Dot Product with Zero Function Yields Zero

Informal description

For any vector $v$ with entries in an additive commutative monoid $\alpha$ with multiplication, the dot product of $v$ with the zero vector (defined as the function mapping every index to $0$) equals the zero element of $\alpha$, i.e., $v \cdot (λ \_. 0) = 0$.

zero_dotProduct theorem

: 0 ⬝ᵥ v = 0

Full source

@[simp]
theorem zero_dotProduct : 0 ⬝ᵥ v = 0 := by simp [dotProduct]

Dot Product with Zero Vector Yields Zero

Informal description

For any vector $v$ with entries in an additive commutative monoid $\alpha$ with multiplication, the dot product of the zero vector with $v$ equals the zero element of $\alpha$, i.e., $0 \cdot v = 0$.

zero_dotProduct' theorem

: (fun _ => (0 : α)) ⬝ᵥ v = 0

Full source

@[simp]
theorem zero_dotProduct' : (fun _ => (0 : α)) ⬝ᵥ v = 0 :=
  zero_dotProduct v

Dot Product with Zero Vector Yields Zero (Constant Zero Version)

Informal description

For any vector $v$ with entries in an additive commutative monoid $\alpha$ with multiplication, the dot product of the zero vector (defined as the constant function $\lambda \_, 0$) with $v$ equals the zero element of $\alpha$, i.e., $0 \cdot v = 0$.

add_dotProduct theorem

: (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w

Full source

@[simp]
theorem add_dotProduct : (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w := by
  simp [dotProduct, add_mul, Finset.sum_add_distrib]

Linearity of Dot Product over Vector Addition (Left)

Informal description

For any vectors $u, v, w : m \to \alpha$ in an additive commutative monoid $\alpha$ with multiplication, the dot product satisfies the linearity property: \[ (u + v) \cdot w = u \cdot w + v \cdot w \] where $\cdot$ denotes the dot product operation.

dotProduct_add theorem

: u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w

Full source

@[simp]
theorem dotProduct_add : u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w := by
  simp [dotProduct, mul_add, Finset.sum_add_distrib]

Linearity of Dot Product over Vector Addition

Informal description

For any vectors $u, v, w : m \to \alpha$ in an additive commutative monoid $\alpha$ with multiplication, the dot product satisfies the linearity property: \[ u \cdot (v + w) = u \cdot v + u \cdot w \] where $\cdot$ denotes the dot product operation.

sumElim_dotProduct_sumElim theorem

: Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y

Full source

@[simp]
theorem sumElim_dotProduct_sumElim : Sum.elimSum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y := by
  simp [dotProduct]

Dot Product of Concatenated Vectors Equals Sum of Dot Products

Informal description

For any vectors $u, v : m \to \alpha$ and $x, y : n \to \alpha$ in an additive commutative monoid $\alpha$ with multiplication, the dot product of the concatenated vectors $\text{Sum.elim}\,u\,x$ and $\text{Sum.elim}\,v\,y$ is equal to the sum of the dot products $u \cdot v$ and $x \cdot y$, i.e., \[ (\text{Sum.elim}\,u\,x) \cdot (\text{Sum.elim}\,v\,y) = u \cdot v + x \cdot y. \]

comp_equiv_symm_dotProduct theorem

(e : m ≃ n) : u ∘ e.symm ⬝ᵥ x = u ⬝ᵥ x ∘ e

Full source

/-- Permuting a vector on the left of a dot product can be transferred to the right. -/
@[simp]
theorem comp_equiv_symm_dotProduct (e : m ≃ n) : u ∘ e.symmu ∘ e.symm ⬝ᵥ x = u ⬝ᵥ x ∘ e :=
  (e.sum_comp _).symm.trans <|
    Finset.sum_congr rfl fun _ _ => by simp only [Function.comp, Equiv.symm_apply_apply]

Dot Product Invariance Under Permutation of Inputs

Informal description

Let $e : m \simeq n$ be an equivalence between finite types $m$ and $n$. For any vectors $u : m \to \alpha$ and $x : n \to \alpha$ in an additive commutative monoid $\alpha$ with multiplication, the dot product of $u \circ e^{-1}$ with $x$ is equal to the dot product of $u$ with $x \circ e$. That is, \[ (u \circ e^{-1}) \cdot x = u \cdot (x \circ e). \]

dotProduct_comp_equiv_symm theorem

(e : n ≃ m) : u ⬝ᵥ x ∘ e.symm = u ∘ e ⬝ᵥ x

Full source

/-- Permuting a vector on the right of a dot product can be transferred to the left. -/
@[simp]
theorem dotProduct_comp_equiv_symm (e : n ≃ m) : u ⬝ᵥ x ∘ e.symm = u ∘ eu ∘ e ⬝ᵥ x := by
  simpa only [Equiv.symm_symm] using (comp_equiv_symm_dotProduct u x e.symm).symm

Dot Product Invariance Under Permutation of Inputs (Symmetric Form)

Informal description

Let $e : n \simeq m$ be an equivalence between finite types $n$ and $m$. For any vectors $u : m \to \alpha$ and $x : n \to \alpha$ in an additive commutative monoid $\alpha$ with multiplication, the dot product of $u$ with $x \circ e^{-1}$ is equal to the dot product of $u \circ e$ with $x$. That is, \[ u \cdot (x \circ e^{-1}) = (u \circ e) \cdot x. \]

comp_equiv_dotProduct_comp_equiv theorem

(e : m ≃ n) : x ∘ e ⬝ᵥ y ∘ e = x ⬝ᵥ y

Full source

/-- Permuting vectors on both sides of a dot product is a no-op. -/
@[simp]
theorem comp_equiv_dotProduct_comp_equiv (e : m ≃ n) : x ∘ ex ∘ e ⬝ᵥ y ∘ e = x ⬝ᵥ y := by
  simp [← dotProduct_comp_equiv_symm, Function.comp_def _ e.symm]

Dot Product Invariance Under Vector Permutation

Informal description

For any bijection $e : m \simeq n$ between finite types $m$ and $n$, and any vectors $x, y : m \to \alpha$ (where $\alpha$ is an additive commutative monoid with multiplication), the dot product of the permuted vectors $x \circ e$ and $y \circ e$ equals the dot product of the original vectors $x$ and $y$, i.e., $$(x \circ e) \cdot (y \circ e) = x \cdot y.$$

diagonal_dotProduct theorem

(i : m) : diagonal v i ⬝ᵥ w = v i * w i

Full source

@[simp]
theorem diagonal_dotProduct (i : m) : diagonaldiagonal v i ⬝ᵥ w = v i * w i := by
  have : ∀ j ≠ i, diagonal v i j * w j = 0 := fun j hij => by
    simp [diagonal_apply_ne' _ hij]
  convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Dot Product of Diagonal Matrix Row: $(\text{diag}(v))_{i,\cdot} \cdot w = v_i w_i$

Informal description

For any index $i$ in a finite type $m$, the dot product of the $i$-th row of the diagonal matrix constructed from a vector $v : m \to \alpha$ with a vector $w : m \to \alpha$ equals the product $v_i w_i$. That is, $(\text{diagonal } v)_{i,\cdot} \cdot w = v_i w_i$.

dotProduct_diagonal theorem

(i : m) : v ⬝ᵥ diagonal w i = v i * w i

Full source

@[simp]
theorem dotProduct_diagonal (i : m) : v ⬝ᵥ diagonal w i = v i * w i := by
  have : ∀ j ≠ i, v j * diagonal w i j = 0 := fun j hij => by
    simp [diagonal_apply_ne' _ hij]
  convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Dot Product with Diagonal Matrix Column: $v \cdot (\text{diag}(w))_{\cdot i} = v_i w_i$

Informal description

For any index $i$ in a finite type $m$, the dot product of a vector $v : m \to \alpha$ with the $i$-th column of the diagonal matrix constructed from a vector $w : m \to \alpha$ equals the product $v_i w_i$. That is, $v \cdot (\text{diag}(w))_{\cdot i} = v_i w_i$.

dotProduct_diagonal' theorem

(i : m) : (v ⬝ᵥ fun j => diagonal w j i) = v i * w i

Full source

@[simp]
theorem dotProduct_diagonal' (i : m) : (v ⬝ᵥ fun j => diagonal w j i) = v i * w i := by
  have : ∀ j ≠ i, v j * diagonal w j i = 0 := fun j hij => by
    simp [diagonal_apply_ne _ hij]
  convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Dot Product with Diagonal Matrix Column: $v \cdot (\text{diag}(w))_{\cdot i} = v_i w_i$

Informal description

For any index $i$ in a finite type $m$, the dot product of a vector $v : m \to \alpha$ with the $i$-th column of the diagonal matrix constructed from a vector $w : m \to \alpha$ equals the product $v_i w_i$. That is, $v \cdot (\text{diagonal } w)_{\cdot i} = v_i w_i$.

single_dotProduct theorem

(x : α) (i : m) : Pi.single i x ⬝ᵥ v = x * v i

Full source

@[simp]
theorem single_dotProduct (x : α) (i : m) : Pi.singlePi.single i x ⬝ᵥ v = x * v i := by
  -- Porting note: (implicit arg) added `(f := fun _ => α)`
  have : ∀ j ≠ i, Pi.single (f := fun _ => α) i x j * v j = 0 := fun j hij => by
    simp [Pi.single_eq_of_ne hij]
  convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Dot Product with Single Nonzero Entry: $(\text{single}_i x) \cdot v = x v_i$

Informal description

For any element $x$ in a type $\alpha$ with multiplication and an additive commutative monoid structure, and for any index $i$ in a finite type $m$, the dot product of the vector $\text{Pi.single}\ i\ x$ (which is $x$ at index $i$ and $0$ elsewhere) with a vector $v : m \to \alpha$ equals $x \cdot v_i$.

dotProduct_single theorem

(x : α) (i : m) : v ⬝ᵥ Pi.single i x = v i * x

Full source

@[simp]
theorem dotProduct_single (x : α) (i : m) : v ⬝ᵥ Pi.single i x = v i * x := by
  -- Porting note: (implicit arg) added `(f := fun _ => α)`
  have : ∀ j ≠ i, v j * Pi.single (f := fun _ => α) i x j = 0 := fun j hij => by
    simp [Pi.single_eq_of_ne hij]
  convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Dot Product with a Single Nonzero Entry: $v \cdot \text{single}_i x = v_i x$

Informal description

For any element $x$ in a type $\alpha$ with multiplication and an additive commutative monoid structure, and for any index $i$ in a finite type $m$, the dot product of a vector $v : m \to \alpha$ with the vector $\text{Pi.single}\ i\ x$ (which is $x$ at index $i$ and $0$ elsewhere) equals $v_i \cdot x$.

one_dotProduct_one theorem

: (1 : n → α) ⬝ᵥ 1 = Fintype.card n

Full source

@[simp]
theorem one_dotProduct_one : (1 : n → α) ⬝ᵥ 1 = Fintype.card n := by
  simp [dotProduct]

Dot Product of Ones Equals Cardinality: $1 \cdot 1 = |n|$

Informal description

For the constant vector $1 : n \to \alpha$ (where every entry is the multiplicative identity $1$), the dot product of $1$ with itself equals the cardinality of the finite type $n$, i.e., $1 \cdot 1 = |n|$.

dotProduct_single_one theorem

[DecidableEq n] (v : n → α) (i : n) : dotProduct v (Pi.single i 1) = v i

Full source

theorem dotProduct_single_one [DecidableEq n] (v : n → α) (i : n) :
    dotProduct v (Pi.single i 1) = v i := by
  rw [dotProduct_single, mul_one]

Dot Product with Standard Basis Vector: $v \cdot e_i = v_i$

Informal description

For any vector $v : n \to \alpha$ in a type $\alpha$ with multiplication and an additive commutative monoid structure, and for any index $i$ in a finite type $n$ with decidable equality, the dot product of $v$ with the vector $\text{Pi.single}\ i\ 1$ (which is $1$ at index $i$ and $0$ elsewhere) equals $v_i$.

single_one_dotProduct theorem

[DecidableEq n] (i : n) (v : n → α) : dotProduct (Pi.single i 1) v = v i

Full source

theorem single_one_dotProduct [DecidableEq n] (i : n) (v : n → α) :
    dotProduct (Pi.single i 1) v = v i := by
  rw [single_dotProduct, one_mul]

Dot Product with Standard Basis Vector: $e_i \cdot v = v_i$

Informal description

For any finite type $n$ with decidable equality, any index $i \in n$, and any vector $v : n \to \alpha$, the dot product of the vector $\text{Pi.single}\ i\ 1$ (which is $1$ at index $i$ and $0$ elsewhere) with $v$ equals $v_i$, i.e., $(\text{single}_i 1) \cdot v = v_i$.

neg_dotProduct theorem

: -v ⬝ᵥ w = -(v ⬝ᵥ w)

Full source

@[simp]
theorem neg_dotProduct : -v ⬝ᵥ w = -(v ⬝ᵥ w) := by simp [dotProduct]

Negation and Dot Product: $-v \cdot w = -(v \cdot w)$

Informal description

For vectors $v, w$ in an additive commutative monoid $\alpha$ with multiplication, the dot product of $-v$ with $w$ equals the negation of the dot product of $v$ with $w$, i.e., $-v \cdot w = -(v \cdot w)$.

dotProduct_neg theorem

: v ⬝ᵥ -w = -(v ⬝ᵥ w)

Full source

@[simp]
theorem dotProduct_neg : v ⬝ᵥ -w = -(v ⬝ᵥ w) := by simp [dotProduct]

Dot Product with Negated Vector: $v \cdot (-w) = -(v \cdot w)$

Informal description

For any vectors $v, w : m \to \alpha$ in an additive commutative monoid $\alpha$ with multiplication, the dot product of $v$ with the negation of $w$ equals the negation of the dot product of $v$ with $w$, i.e., $v \cdot (-w) = -(v \cdot w)$.

neg_dotProduct_neg theorem

: -v ⬝ᵥ -w = v ⬝ᵥ w

Full source

lemma neg_dotProduct_neg : -v ⬝ᵥ -w = v ⬝ᵥ w := by
  rw [neg_dotProduct, dotProduct_neg, neg_neg]

Dot Product of Negated Vectors: $-v \cdot -w = v \cdot w$

Informal description

For any vectors $v, w : m \to \alpha$ in an additive commutative monoid $\alpha$ with multiplication, the dot product of $-v$ with $-w$ equals the dot product of $v$ with $w$, i.e., $-v \cdot -w = v \cdot w$.

sub_dotProduct theorem

: (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w

Full source

@[simp]
theorem sub_dotProduct : (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w := by simp [sub_eq_add_neg]

Linearity of Dot Product over Vector Subtraction (Left)

Informal description

For any vectors $u, v, w : m \to \alpha$ in an additive commutative monoid $\alpha$ with multiplication, the dot product satisfies the linearity property with respect to vector subtraction: \[ (u - v) \cdot w = u \cdot w - v \cdot w \] where $\cdot$ denotes the dot product operation.

dotProduct_sub theorem

: u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w

Full source

@[simp]
theorem dotProduct_sub : u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w := by simp [sub_eq_add_neg]

Dot Product Distributes over Vector Subtraction: $u \cdot (v - w) = u \cdot v - u \cdot w$

Informal description

For any vectors $u, v, w : m \to \alpha$ in an additive commutative monoid $\alpha$ with multiplication, the dot product satisfies the linearity property with respect to vector subtraction: \[ u \cdot (v - w) = u \cdot v - u \cdot w \] where $\cdot$ denotes the dot product operation.

smul_dotProduct theorem

[IsScalarTower R α α] (x : R) (v w : m → α) : x • v ⬝ᵥ w = x • (v ⬝ᵥ w)

Full source

@[simp]
theorem smul_dotProduct [IsScalarTower R α α] (x : R) (v w : m → α) :
    x • v ⬝ᵥ w = x • (v ⬝ᵥ w) := by simp [dotProduct, Finset.smul_sum, smul_mul_assoc]

Scalar Multiplication Commutes with Dot Product: $(x \cdot v) \cdot w = x \cdot (v \cdot w)$

Informal description

Let $R$ and $\alpha$ be types such that $\alpha$ is an additive commutative monoid with a scalar multiplication by $R$ satisfying the compatibility condition `IsScalarTower R α α`. For any scalar $x \in R$ and vectors $v, w : m \to \alpha$, the dot product of $x \cdot v$ with $w$ is equal to $x$ multiplied by the dot product of $v$ with $w$, i.e., $$(x \cdot v) \cdot w = x \cdot (v \cdot w).$$

dotProduct_smul theorem

[SMulCommClass R α α] (x : R) (v w : m → α) : v ⬝ᵥ x • w = x • (v ⬝ᵥ w)

Full source

@[simp]
theorem dotProduct_smul [SMulCommClass R α α] (x : R) (v w : m → α) :
    v ⬝ᵥ x • w = x • (v ⬝ᵥ w) := by simp [dotProduct, Finset.smul_sum, mul_smul_comm]

Dot Product Commutes with Scalar Multiplication: $v \cdot (x \cdot w) = x \cdot (v \cdot w)$

Informal description

Let $R$ and $\alpha$ be types such that $\alpha$ is an additive commutative monoid with a scalar multiplication by $R$ satisfying the compatibility condition `SMulCommClass R α α`. For any scalar $x \in R$ and vectors $v, w : m \to \alpha$, the dot product of $v$ with $x \cdot w$ is equal to $x$ multiplied by the dot product of $v$ with $w$, i.e., $$v \cdot (x \cdot w) = x \cdot (v \cdot w).$$

Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instance

[Fintype m] [Mul α] [AddCommMonoid α] : HMul (Matrix l m α) (Matrix m n α) (Matrix l n α)

Full source

/-- `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. -/
-- We want to be lower priority than `instHMul`, but without this we can't have operands with
-- implicit dimensions.
@[default_instance 100]
instance [Fintype m] [Mul α] [AddCommMonoid α] :
    HMul (Matrix l m α) (Matrix m n α) (Matrix l n α) where
  hMul M N := fun i k => (fun j => M i j) ⬝ᵥ fun j => N j k

Matrix Multiplication for Finite-Dimensional Matrices

Informal description

For any finite type $m$, type $\alpha$ with multiplication and an additive commutative monoid structure, the type of matrices $\mathrm{Matrix}\, l\, m\, \alpha$ is equipped with a multiplication operation with $\mathrm{Matrix}\, m\, n\, \alpha$, resulting in a matrix of type $\mathrm{Matrix}\, l\, n\, \alpha$. The product $M * N$ of two matrices $M$ and $N$ is defined such that the $(i,k)$-th entry of $M * N$ is the dot product of the $i$-th row of $M$ with the $k$-th column of $N$, i.e., $(M * N)_{i,k} = \sum_j M_{i,j} N_{j,k}$.

Matrix.mul_apply theorem

 [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i k} : (M * N) i k = ∑ j, M i j * N j k

Full source

theorem mul_apply [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α}
    {i k} : (M * N) i k = ∑ j, M i j * N j k :=
  rfl

Matrix Multiplication Entry Formula: $(M * N)_{i,k} = \sum_j M_{i,j} N_{j,k}$

Informal description

Let $m$ be a finite type, $\alpha$ a type with multiplication and an additive commutative monoid structure, and $M : \mathrm{Matrix}\, l\, m\, \alpha$, $N : \mathrm{Matrix}\, m\, n\, \alpha$ be matrices. For any indices $i$ and $k$, the $(i,k)$-th entry of the matrix product $M * N$ is given by the sum over $j$ of the products of the corresponding entries of $M$ and $N$: $$(M * N)_{i,k} = \sum_j M_{i,j} N_{j,k}.$$

Matrix.instMulOfFintypeOfAddCommMonoid instance

[Fintype n] [Mul α] [AddCommMonoid α] : Mul (Matrix n n α)

Full source

instance [Fintype n] [Mul α] [AddCommMonoid α] : Mul (Matrix n n α) where mul M N := M * N

Square Matrices Form a Multiplicative Monoid

Informal description

For any finite type $n$ and type $\alpha$ equipped with multiplication and an additive commutative monoid structure, the set of square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ forms a multiplicative monoid. The multiplication operation is defined by the standard matrix multiplication formula: for two matrices $A$ and $B$, the $(i,k)$-th entry of $A * B$ is given by $\sum_j A_{i,j} \cdot B_{j,k}$.

Matrix.mul_apply' theorem

 [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i k} :
  (M * N) i k = (fun j => M i j) ⬝ᵥ fun j => N j k

Full source

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

Matrix Multiplication Entry Formula via Dot Product

Informal description

Let $m$ be a finite type, $\alpha$ a type with multiplication and an additive commutative monoid structure, and $M : \mathrm{Matrix}\, l\, m\, \alpha$, $N : \mathrm{Matrix}\, m\, n\, \alpha$ be matrices. For any indices $i$ and $k$, the $(i,k)$-th entry of the matrix product $M * N$ is equal to the dot product of the $i$-th row of $M$ and the $k$-th column of $N$: $$(M * N)_{i,k} = \sum_j M_{i,j} N_{j,k}.$$

Matrix.two_mul_expl theorem

 {R : Type*} [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

Full source

theorem two_mul_expl {R : Type*} [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 := by
  refine ⟨?_, ?_, ?_, ?_⟩ <;>
  · rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
    simp

Explicit Formula for $2 \times 2$ Matrix Multiplication

Informal description

Let $R$ be a non-unital, non-associative semiring, and let $A, B$ be $2 \times 2$ matrices over $R$. Then the entries of the matrix product $A * B$ are given by: \begin{align*} (A * B)_{0,0} &= A_{0,0} \cdot B_{0,0} + A_{0,1} \cdot B_{1,0}, \\ (A * B)_{0,1} &= A_{0,0} \cdot B_{0,1} + A_{0,1} \cdot B_{1,1}, \\ (A * B)_{1,0} &= A_{1,0} \cdot B_{0,0} + A_{1,1} \cdot B_{1,0}, \\ (A * B)_{1,1} &= A_{1,0} \cdot B_{0,1} + A_{1,1} \cdot B_{1,1}. \end{align*}

Matrix.smul_mul theorem

 [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] (a : R) (M : Matrix m n α) (N : Matrix n l α) :
  (a • M) * N = a • (M * N)

Full source

@[simp]
theorem smul_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) := by
  ext
  apply smul_dotProduct a

Scalar Multiplication Distributes Over Matrix Multiplication: $(a \cdot M) * N = a \cdot (M * N)$

Informal description

Let $R$ be a monoid acting distributively on an additive commutative monoid $\alpha$, with the scalar multiplication satisfying the compatibility condition `IsScalarTower R α α`. For any finite type $n$, scalar $a \in R$, matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$, and matrix $N \in \mathrm{Matrix}\, n\, l\, \alpha$, the matrix product of the scalar multiple $a \cdot M$ with $N$ is equal to the scalar multiple $a$ applied to the matrix product $M * N$, i.e., $$(a \cdot M) * N = a \cdot (M * N).$$

Matrix.mul_smul theorem

 [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α] (M : Matrix m n α) (a : R) (N : Matrix n l α) :
  M * (a • N) = a • (M * N)

Full source

@[simp]
theorem mul_smul [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α]
    (M : Matrix m n α) (a : R) (N : Matrix n l α) : M * (a • N) = a • (M * N) := by
  ext
  apply dotProduct_smul

Matrix multiplication commutes with scalar multiplication: $M * (a \cdot N) = a \cdot (M * N)$

Informal description

Let $R$ be a monoid and $\alpha$ be a type equipped with a distributive multiplicative action by $R$ and a scalar multiplication operation that commutes with the multiplication in $\alpha$. For any finite type $n$, scalar $a \in R$, and matrices $M \in \text{Matrix}\, m\, n\, \alpha$ and $N \in \text{Matrix}\, n\, l\, \alpha$, the matrix product $M * (a \cdot N)$ is equal to $a \cdot (M * N)$.

Matrix.mul_zero theorem

[Fintype n] (M : Matrix m n α) : M * (0 : Matrix n o α) = 0

Full source

@[simp]
protected theorem mul_zero [Fintype n] (M : Matrix m n α) : M * (0 : Matrix n o α) = 0 := by
  ext
  apply dotProduct_zero

Right Multiplication by Zero Matrix Yields Zero Matrix

Informal description

For any finite type $n$ and matrix $M$ of type $\mathrm{Matrix}\, m\, n\, \alpha$, the product of $M$ with the zero matrix of type $\mathrm{Matrix}\, n\, o\, \alpha$ is the zero matrix of type $\mathrm{Matrix}\, m\, o\, \alpha$, i.e., $M \cdot 0 = 0$.

Matrix.zero_mul theorem

[Fintype m] (M : Matrix m n α) : (0 : Matrix l m α) * M = 0

Full source

@[simp]
protected theorem zero_mul [Fintype m] (M : Matrix m n α) : (0 : Matrix l m α) * M = 0 := by
  ext
  apply zero_dotProduct

Left Multiplication by Zero Matrix Yields Zero Matrix

Informal description

For any finite type $m$ and any type $\alpha$ with a zero element, the product of the zero matrix in $\mathrm{Matrix}\, l\, m\, \alpha$ with any matrix $M$ in $\mathrm{Matrix}\, m\, n\, \alpha$ is the zero matrix in $\mathrm{Matrix}\, l\, n\, \alpha$, i.e., $0 * M = 0$.

Matrix.mul_add theorem

[Fintype n] (L : Matrix m n α) (M N : Matrix n o α) : L * (M + N) = L * M + L * N

Full source

protected theorem mul_add [Fintype n] (L : Matrix m n α) (M N : Matrix n o α) :
    L * (M + N) = L * M + L * N := by
  ext
  apply dotProduct_add

Distributivity of Matrix Multiplication over Addition: $L * (M + N) = L * M + L * N$

Informal description

For any finite type $n$, type $\alpha$ with multiplication and an additive commutative monoid structure, and matrices $L \in \mathrm{Matrix}\, m\, n\, \alpha$, $M, N \in \mathrm{Matrix}\, n\, o\, \alpha$, the following equality holds: \[ L * (M + N) = L * M + L * N \] where $*$ denotes matrix multiplication and $+$ denotes componentwise matrix addition.

Matrix.add_mul theorem

[Fintype m] (L M : Matrix l m α) (N : Matrix m n α) : (L + M) * N = L * N + M * N

Full source

protected theorem add_mul [Fintype m] (L M : Matrix l m α) (N : Matrix m n α) :
    (L + M) * N = L * N + M * N := by
  ext
  apply add_dotProduct

Left Distributivity of Matrix Multiplication over Addition: $(L + M) * N = L * N + M * N$

Informal description

For any finite type $m$, types $l$ and $n$, and a type $\alpha$ with addition and multiplication forming an additive commutative monoid, let $L$ and $M$ be matrices in $\mathrm{Matrix}\, l\, m\, \alpha$ and $N$ be a matrix in $\mathrm{Matrix}\, m\, n\, \alpha$. Then the matrix multiplication satisfies the left distributivity property: \[ (L + M) * N = L * N + M * N \] where $*$ denotes matrix multiplication and $+$ denotes componentwise matrix addition.

Matrix.nonUnitalNonAssocSemiring instance

[Fintype n] : NonUnitalNonAssocSemiring (Matrix n n α)

Full source

instance nonUnitalNonAssocSemiring [Fintype n] : NonUnitalNonAssocSemiring (Matrix n n α) :=
  { Matrix.addCommMonoid with
    mul_zero := Matrix.mul_zero
    zero_mul := Matrix.zero_mul
    left_distrib := Matrix.mul_add
    right_distrib := Matrix.add_mul }

Square Matrices Form a Non-Unital Non-Associative Semiring

Informal description

For any finite type $n$ and type $\alpha$ with multiplication and an additive commutative monoid structure, the set of square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ forms a non-unital non-associative semiring. The operations are defined as follows: - Addition is componentwise and forms a commutative monoid. - Multiplication is given by standard matrix multiplication: $(A * B)_{i,j} = \sum_k A_{i,k} \cdot B_{k,j}$. - The multiplication is distributive over addition but does not necessarily have a multiplicative identity or satisfy associativity.

Matrix.diagonal_mul theorem

[Fintype m] [DecidableEq m] (d : m → α) (M : Matrix m n α) (i j) : (diagonal d * M) i j = d i * M i j

Full source

@[simp]
theorem diagonal_mul [Fintype m] [DecidableEq m] (d : m → α) (M : Matrix m n α) (i j) :
    (diagonal d * M) i j = d i * M i j :=
  diagonal_dotProduct _ _ _

Diagonal Matrix Multiplication: $(\text{diag}(d) * M)_{i,j} = d_i M_{i,j}$

Informal description

Let $m$ be a finite type with decidable equality, and let $\alpha$ be a type equipped with multiplication and an additive commutative monoid structure. For any diagonal matrix $\text{diag}(d)$ constructed from a vector $d : m \to \alpha$ and any matrix $M : \text{Matrix}\, m\, n\, \alpha$, the $(i,j)$-th entry of the product $\text{diag}(d) * M$ is given by $d_i \cdot M_{i,j}$.

Matrix.mul_diagonal theorem

[Fintype n] [DecidableEq n] (d : n → α) (M : Matrix m n α) (i j) : (M * diagonal d) i j = M i j * d j

Full source

@[simp]
theorem mul_diagonal [Fintype n] [DecidableEq n] (d : n → α) (M : Matrix m n α) (i j) :
    (M * diagonal d) i j = M i j * d j := by
  rw [← diagonal_transpose]
  apply dotProduct_diagonal

Right Multiplication by Diagonal Matrix: $(M \cdot \text{diag}(d))_{i,j} = M_{i,j} d_j$

Informal description

Let $m$ and $n$ be finite types with decidable equality, and let $\alpha$ be a type with multiplication and an additive commutative monoid structure. For any diagonal matrix $\text{diag}(d)$ constructed from a vector $d : n \to \alpha$ and any matrix $M \in \text{Matrix}\, m\, n\, \alpha$, the $(i,j)$-th entry of the product matrix $M \cdot \text{diag}(d)$ is equal to $M_{i,j} \cdot d_j$.

Matrix.diagonal_mul_diagonal theorem

[Fintype n] [DecidableEq n] (d₁ d₂ : n → α) : diagonal d₁ * diagonal d₂ = diagonal fun i => d₁ i * d₂ i

Full source

@[simp]
theorem diagonal_mul_diagonal [Fintype n] [DecidableEq n] (d₁ d₂ : n → α) :
    diagonal d₁ * diagonal d₂ = diagonal fun i => d₁ i * d₂ i := by
  ext i j
  by_cases h : i = j <;>
  simp [h]

Product of Diagonal Matrices is Pointwise Product: $\text{diag}(d_1) \cdot \text{diag}(d_2) = \text{diag}(d_1 \cdot d_2)$

Informal description

Let $n$ be a finite type with decidable equality, and let $\alpha$ be a type equipped with multiplication and an additive commutative monoid structure. For any two vectors $d_1, d_2 : n \to \alpha$, the product of the diagonal matrices $\text{diag}(d_1)$ and $\text{diag}(d_2)$ is equal to the diagonal matrix whose entries are the pointwise product of $d_1$ and $d_2$, i.e., \[ \text{diag}(d_1) \cdot \text{diag}(d_2) = \text{diag}(i \mapsto d_1(i) \cdot d_2(i)). \]

Matrix.diagonal_mul_diagonal' theorem

[Fintype n] [DecidableEq n] (d₁ d₂ : n → α) : diagonal d₁ * diagonal d₂ = diagonal fun i => d₁ i * d₂ i

Full source

theorem diagonal_mul_diagonal' [Fintype n] [DecidableEq n] (d₁ d₂ : n → α) :
    diagonal d₁ * diagonal d₂ = diagonal fun i => d₁ i * d₂ i :=
  diagonal_mul_diagonal _ _

Product of Diagonal Matrices is Pointwise Product: $\text{diag}(d_1) \cdot \text{diag}(d_2) = \text{diag}(d_1 \cdot d_2)$

Informal description

Let $n$ be a finite type with decidable equality, and let $\alpha$ be a type equipped with multiplication and an additive commutative monoid structure. For any two vectors $d_1, d_2 : n \to \alpha$, the product of the diagonal matrices $\text{diag}(d_1)$ and $\text{diag}(d_2)$ is equal to the diagonal matrix whose entries are the pointwise product of $d_1$ and $d_2$, i.e., \[ \text{diag}(d_1) \cdot \text{diag}(d_2) = \text{diag}(i \mapsto d_1(i) \cdot d_2(i)). \]

Matrix.smul_eq_diagonal_mul theorem

[Fintype m] [DecidableEq m] (M : Matrix m n α) (a : α) : a • M = (diagonal fun _ => a) * M

Full source

theorem smul_eq_diagonal_mul [Fintype m] [DecidableEq m] (M : Matrix m n α) (a : α) :
    a • M = (diagonal fun _ => a) * M := by
  ext
  simp

Scalar Multiplication as Diagonal Matrix Multiplication: $a \cdot M = \text{diag}(a) * M$

Informal description

Let $m$ be a finite type with decidable equality, and let $\alpha$ be a type with scalar multiplication. For any matrix $M \in \text{Matrix}\, m\, n\, \alpha$ and scalar $a \in \alpha$, the scalar multiplication $a \cdot M$ is equal to the matrix product of the diagonal matrix $\text{diag}(a)$ (where all diagonal entries are $a$) with $M$. That is, $a \cdot M = \text{diag}(a) * M$.

Matrix.op_smul_eq_mul_diagonal theorem

[Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) : MulOpposite.op a • M = M * (diagonal fun _ : n => a)

Full source

theorem op_smul_eq_mul_diagonal [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) :
    MulOpposite.op a • M = M * (diagonal fun _ : n => a) := by
  ext
  simp

Scalar Multiplication in Opposite Algebra Equals Right Multiplication by Diagonal Matrix

Informal description

Let $m$ and $n$ be finite types with decidable equality, and let $\alpha$ be a type with multiplication and an additive commutative monoid structure. For any matrix $M \in \text{Matrix}\, m\, n\, \alpha$ and any scalar $a \in \alpha$, the scalar multiplication of $M$ by $a$ in the multiplicative opposite $\alpha^\text{op}$ is equal to the matrix product of $M$ with the diagonal matrix where all diagonal entries are $a$. That is, $\text{op}(a) \cdot M = M \cdot \text{diag}(\lambda \_. a)$.

Matrix.addMonoidHomMulLeft definition

[Fintype m] (M : Matrix l m α) : Matrix m n α →+ Matrix l n α

Full source

/-- Left multiplication by a matrix, as an `AddMonoidHom` from matrices to matrices. -/
@[simps]
def addMonoidHomMulLeft [Fintype m] (M : Matrix l m α) : MatrixMatrix m n α →+ Matrix l n α where
  toFun x := M * x
  map_zero' := Matrix.mul_zero _
  map_add' := Matrix.mul_add _

Left multiplication by a matrix as an additive monoid homomorphism

Informal description

For a finite type `m`, given a matrix `M` of type `Matrix l m α`, the function `Matrix.addMonoidHomMulLeft M` is an additive monoid homomorphism from `Matrix m n α` to `Matrix l n α` defined by left multiplication by `M`. That is, it maps a matrix `x` to the matrix product `M * x`, preserving addition and the zero matrix.

Matrix.addMonoidHomMulRight definition

[Fintype m] (M : Matrix m n α) : Matrix l m α →+ Matrix l n α

Full source

/-- Right multiplication by a matrix, as an `AddMonoidHom` from matrices to matrices. -/
@[simps]
def addMonoidHomMulRight [Fintype m] (M : Matrix m n α) : MatrixMatrix l m α →+ Matrix l n α where
  toFun x := x * M
  map_zero' := Matrix.zero_mul _
  map_add' _ _ := Matrix.add_mul _ _ _

Right multiplication by a matrix as an additive monoid homomorphism

Informal description

For a finite type $ m $ and matrices $ M \in \mathrm{Matrix}\, m\, n\, \alpha $, the function $ \mathrm{Matrix.addMonoidHomMulRight}\, M $ is the additive monoid homomorphism from $ \mathrm{Matrix}\, l\, m\, \alpha $ to $ \mathrm{Matrix}\, l\, n\, \alpha $ defined by right multiplication by $ M $. That is, it maps a matrix $ x $ to $ x * M $, preserving addition and the zero matrix.

Matrix.sum_mul theorem

 [Fintype m] (s : Finset β) (f : β → Matrix l m α) (M : Matrix m n α) : (∑ a ∈ s, f a) * M = ∑ a ∈ s, f a * M

Full source

protected theorem sum_mul [Fintype m] (s : Finset β) (f : β → Matrix l m α) (M : Matrix m n α) :
    (∑ a ∈ s, f a) * M = ∑ a ∈ s, f a * M :=
  map_sum (addMonoidHomMulRight M) f s

Linearity of Matrix Multiplication over Finite Sums

Informal description

Let $m$ be a finite type, and let $\alpha$ be a type equipped with multiplication and an additive commutative monoid structure. For any finite set $s$ indexed by $\beta$, any family of matrices $f : \beta \to \mathrm{Matrix}\, l\, m\, \alpha$, and any matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$, we have \[ \left(\sum_{a \in s} f(a)\right) * M = \sum_{a \in s} (f(a) * M). \]

Matrix.mul_sum theorem

 [Fintype m] (s : Finset β) (f : β → Matrix m n α) (M : Matrix l m α) : (M * ∑ a ∈ s, f a) = ∑ a ∈ s, M * f a

Full source

protected theorem mul_sum [Fintype m] (s : Finset β) (f : β → Matrix m n α) (M : Matrix l m α) :
    (M * ∑ a ∈ s, f a) = ∑ a ∈ s, M * f a :=
  map_sum (addMonoidHomMulLeft M) f s

Distributivity of Matrix Multiplication over Finite Sums

Informal description

Let $m$ be a finite type, and let $\alpha$ be a type equipped with a multiplication operation and an additive commutative monoid structure. For any finite set $s$ of indices $\beta$, any family of matrices $f \colon \beta \to \mathrm{Matrix}\, m\, n\, \alpha$, and any matrix $M \in \mathrm{Matrix}\, l\, m\, \alpha$, the following equality holds: \[ M \cdot \left( \sum_{a \in s} f(a) \right) = \sum_{a \in s} (M \cdot f(a)), \] where $\cdot$ denotes matrix multiplication and the sums are entrywise.

Matrix.Semiring.isScalarTower instance

 [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] : IsScalarTower R (Matrix n n α) (Matrix n n α)

Full source

/-- This instance enables use with `smul_mul_assoc`. -/
instance Semiring.isScalarTower [Fintype n] [Monoid R] [DistribMulAction R α]
    [IsScalarTower R α α] : IsScalarTower R (Matrix n n α) (Matrix n n α) :=
  ⟨fun r m n => Matrix.smul_mul r m n⟩

Scalar Tower Property for Square Matrices

Informal description

For any finite type $n$, monoid $R$, and type $\alpha$ with a distributive multiplicative action of $R$ that forms a scalar tower $R \to \alpha \to \alpha$, the square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ also form a scalar tower with $R$ acting on them. That is, for any $r \in R$ and matrices $A, B \in \mathrm{Matrix}\, n\, n\, \alpha$, we have $r \cdot (A * B) = (r \cdot A) * B = A * (r \cdot B)$.

Matrix.Semiring.smulCommClass instance

 [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α] : SMulCommClass R (Matrix n n α) (Matrix n n α)

Full source

/-- This instance enables use with `mul_smul_comm`. -/
instance Semiring.smulCommClass [Fintype n] [Monoid R] [DistribMulAction R α]
    [SMulCommClass R α α] : SMulCommClass R (Matrix n n α) (Matrix n n α) :=
  ⟨fun r m n => (Matrix.mul_smul m r n).symm⟩

Commutativity of Scalar Multiplication with Matrix Multiplication in Square Matrices

Informal description

For any finite type $n$, monoid $R$, and type $\alpha$ equipped with a distributive multiplicative action by $R$ and a scalar multiplication operation that commutes with the multiplication in $\alpha$, the scalar multiplication operation on square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ commutes with matrix multiplication. That is, for any scalar $r \in R$ and matrices $A, B \in \mathrm{Matrix}\, n\, n\, \alpha$, we have $r \cdot (A * B) = (r \cdot A) * B = A * (r \cdot B)$.

Matrix.one_mul theorem

[Fintype m] [DecidableEq m] (M : Matrix m n α) : (1 : Matrix m m α) * M = M

Full source

@[simp]
protected theorem one_mul [Fintype m] [DecidableEq m] (M : Matrix m n α) :
    (1 : Matrix m m α) * M = M := by
  ext
  rw [← diagonal_one, diagonal_mul, one_mul]

Left Identity Property of Matrix Multiplication: $1 \cdot M = M$

Informal description

Let $m$ be a finite type with decidable equality, and let $\alpha$ be a type with a multiplicative identity. For any matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$, the product of the identity matrix $1 \in \mathrm{Matrix}\, m\, m\, \alpha$ with $M$ equals $M$, i.e., $1 \cdot M = M$.

Matrix.mul_one theorem

[Fintype n] [DecidableEq n] (M : Matrix m n α) : M * (1 : Matrix n n α) = M

Full source

@[simp]
protected theorem mul_one [Fintype n] [DecidableEq n] (M : Matrix m n α) :
    M * (1 : Matrix n n α) = M := by
  ext
  rw [← diagonal_one, mul_diagonal, mul_one]

Right Identity Property of Matrix Multiplication: $M \cdot I = M$

Informal description

Let $m$ and $n$ be finite types with decidable equality, and let $\alpha$ be a type with a multiplicative identity. For any matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$, the product of $M$ with the identity matrix of size $n \times n$ equals $M$, i.e., \[ M \cdot I_n = M. \]

Matrix.nonAssocSemiring instance

[Fintype n] [DecidableEq n] : NonAssocSemiring (Matrix n n α)

Full source

instance nonAssocSemiring [Fintype n] [DecidableEq n] : NonAssocSemiring (Matrix n n α) :=
  { Matrix.nonUnitalNonAssocSemiring, Matrix.instAddCommMonoidWithOne with
    one := 1
    one_mul := Matrix.one_mul
    mul_one := Matrix.mul_one }

Square Matrices Form a Non-Associative Semiring

Informal description

For any finite type $n$ with decidable equality and any type $\alpha$ with a non-associative semiring structure, the square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ form a non-associative semiring. The operations are defined as follows: - Addition is componentwise and forms a commutative monoid. - Multiplication is given by standard matrix multiplication: $(A * B)_{i,j} = \sum_k A_{i,k} \cdot B_{k,j}$. - The multiplication is distributive over addition and has a multiplicative identity given by the identity matrix (with ones on the diagonal and zeros elsewhere).

Matrix.map_mul theorem

 [Fintype n] {L : Matrix m n α} {M : Matrix n o α} [NonAssocSemiring β] {f : α →+* β} :
  (L * M).map f = L.map f * M.map f

Full source

@[simp]
protected theorem map_mul [Fintype n] {L : Matrix m n α} {M : Matrix n o α} [NonAssocSemiring β]
    {f : α →+* β} : (L * M).map f = L.map f * M.map f := by
  ext
  simp [mul_apply, map_sum]

Ring Homomorphism Commutes with Matrix Multiplication: $f(L * M) = f(L) * f(M)$

Informal description

Let $m$, $n$, and $o$ be finite types, and let $L \in \mathrm{Matrix}\, m\, n\, \alpha$ and $M \in \mathrm{Matrix}\, n\, o\, \alpha$ be matrices. Suppose $\beta$ is a non-associative semiring and $f \colon \alpha \to \beta$ is a ring homomorphism. Then the entry-wise application of $f$ to the matrix product $L * M$ equals the matrix product of the entry-wise applications of $f$ to $L$ and $M$, i.e., \[ f(L * M) = f(L) * f(M). \]

Matrix.smul_one_eq_diagonal theorem

[DecidableEq m] (a : α) : a • (1 : Matrix m m α) = diagonal fun _ => a

Full source

theorem smul_one_eq_diagonal [DecidableEq m] (a : α) :
    a • (1 : Matrix m m α) = diagonal fun _ => a := by
  simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, smul_eq_mul, mul_one]

Scalar Multiplication of Identity Matrix Yields Diagonal Matrix: $a \cdot I = \text{diag}(a)$

Informal description

For any type $m$ with decidable equality and any element $a$ of type $\alpha$, the scalar multiplication of $a$ with the identity matrix of size $m \times m$ is equal to the diagonal matrix where every diagonal entry is $a$. That is, $a \cdot I = \text{diag}(a, a, \dots, a)$.

Matrix.op_smul_one_eq_diagonal theorem

[DecidableEq m] (a : α) : MulOpposite.op a • (1 : Matrix m m α) = diagonal fun _ => a

Full source

theorem op_smul_one_eq_diagonal [DecidableEq m] (a : α) :
    MulOpposite.op a • (1 : Matrix m m α) = diagonal fun _ => a := by
  simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, op_smul_eq_mul, one_mul]

Scalar Multiplication by Opposite Element: $\text{op}(a) \cdot I = \text{diag}(a)$

Informal description

For any type $m$ with decidable equality and any element $a$ of type $\alpha$, the scalar multiplication of the multiplicative opposite of $a$ with the identity matrix of size $m \times m$ is equal to the diagonal matrix where every diagonal entry is $a$. That is, $\text{op}(a) \cdot I = \text{diag}(a, a, \dots, a)$.

Matrix.mul_assoc theorem

(L : Matrix l m α) (M : Matrix m n α) (N : Matrix n o α) : L * M * N = L * (M * N)

Full source

protected theorem mul_assoc (L : Matrix l m α) (M : Matrix m n α) (N : Matrix n o α) :
    L * M * N = L * (M * N) := by
  ext
  apply dotProduct_assoc

Associativity of Matrix Multiplication: $(LM)N = L(MN)$

Informal description

Let $\alpha$ be a type with multiplication and an additive commutative monoid structure, and let $l, m, n, o$ be types with $m$ and $n$ finite. For any matrices $L \in \mathrm{Matrix}\, l\, m\, \alpha$, $M \in \mathrm{Matrix}\, m\, n\, \alpha$, and $N \in \mathrm{Matrix}\, n\, o\, \alpha$, the matrix multiplication is associative: \[ (L * M) * N = L * (M * N). \]

Matrix.nonUnitalSemiring instance

: NonUnitalSemiring (Matrix n n α)

Full source

instance nonUnitalSemiring : NonUnitalSemiring (Matrix n n α) :=
  { Matrix.nonUnitalNonAssocSemiring with mul_assoc := Matrix.mul_assoc }

Square Matrices Form a Non-Unital Semiring

Informal description

For any type $n$ and type $\alpha$ with multiplication and an additive commutative monoid structure, the set of square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ forms a non-unital semiring. The operations are defined as follows: - Addition is componentwise and forms a commutative monoid. - Multiplication is given by standard matrix multiplication: $(A * B)_{i,j} = \sum_k A_{i,k} \cdot B_{k,j}$. - The multiplication is distributive over addition and associative, but does not necessarily have a multiplicative identity.

Matrix.semiring instance

[Fintype n] [DecidableEq n] : Semiring (Matrix n n α)

Full source

instance semiring [Fintype n] [DecidableEq n] : Semiring (Matrix n n α) :=
  { Matrix.nonUnitalSemiring, Matrix.nonAssocSemiring with }

Square Matrices Form a Semiring

Informal description

For any finite type $n$ with decidable equality and any type $\alpha$ with a semiring structure, the square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ form a semiring. The operations are defined as follows: - Addition is componentwise and forms a commutative monoid. - Multiplication is given by standard matrix multiplication: $(A * B)_{i,j} = \sum_k A_{i,k} \cdot B_{k,j}$. - The multiplication is associative, distributive over addition, and has a multiplicative identity given by the identity matrix (with ones on the diagonal and zeros elsewhere).

Matrix.neg_mul theorem

(M : Matrix m n α) (N : Matrix n o α) : (-M) * N = -(M * N)

Full source

@[simp]
protected theorem neg_mul (M : Matrix m n α) (N : Matrix n o α) : (-M) * N = -(M * N) := by
  ext
  apply neg_dotProduct

Negation and Matrix Multiplication: $(-M)N = -(MN)$

Informal description

For any matrices $M \in \mathrm{Matrix}\, m\, n\, \alpha$ and $N \in \mathrm{Matrix}\, n\, o\, \alpha$ over a type $\alpha$ with negation and matrix multiplication, the product of the negation of $M$ with $N$ equals the negation of the product of $M$ with $N$, i.e., $(-M) * N = -(M * N)$.

Matrix.mul_neg theorem

(M : Matrix m n α) (N : Matrix n o α) : M * (-N) = -(M * N)

Full source

@[simp]
protected theorem mul_neg (M : Matrix m n α) (N : Matrix n o α) : M * (-N) = -(M * N) := by
  ext
  apply dotProduct_neg

Matrix multiplication with negated matrix: $M \cdot (-N) = -(M \cdot N)$

Informal description

For any matrices $M \in \mathrm{Matrix}\, m\, n\, \alpha$ and $N \in \mathrm{Matrix}\, n\, o\, \alpha$ over a type $\alpha$ with multiplication and an additive commutative monoid structure, the product of $M$ with the negation of $N$ equals the negation of the product of $M$ with $N$, i.e., $M \cdot (-N) = -(M \cdot N)$.

Matrix.sub_mul theorem

(M M' : Matrix m n α) (N : Matrix n o α) : (M - M') * N = M * N - M' * N

Full source

protected theorem sub_mul (M M' : Matrix m n α) (N : Matrix n o α) :
    (M - M') * N = M * N - M' * N := by
  rw [sub_eq_add_neg, Matrix.add_mul, Matrix.neg_mul, sub_eq_add_neg]

Left Distributivity of Matrix Multiplication over Subtraction: $(M - M')N = MN - M'N$

Informal description

For any matrices $M, M' \in \mathrm{Matrix}\, m\, n\, \alpha$ and $N \in \mathrm{Matrix}\, n\, o\, \alpha$ over a type $\alpha$ with subtraction and matrix multiplication, the product of the difference $M - M'$ with $N$ equals the difference of the products $M * N$ and $M' * N$, i.e., $(M - M') * N = M * N - M' * N$.

Matrix.mul_sub theorem

(M : Matrix m n α) (N N' : Matrix n o α) : M * (N - N') = M * N - M * N'

Full source

protected theorem mul_sub (M : Matrix m n α) (N N' : Matrix n o α) :
    M * (N - N') = M * N - M * N' := by
  rw [sub_eq_add_neg, Matrix.mul_add, Matrix.mul_neg, sub_eq_add_neg]

Right Distributivity of Matrix Multiplication over Subtraction: $M \cdot (N - N') = M \cdot N - M \cdot N'$

Informal description

For any matrices $M \in \mathrm{Matrix}\, m\, n\, \alpha$ and $N, N' \in \mathrm{Matrix}\, n\, o\, \alpha$ over a type $\alpha$ with multiplication and an additive commutative monoid structure, the following equality holds: \[ M \cdot (N - N') = M \cdot N - M \cdot N' \] where $\cdot$ denotes matrix multiplication and $-$ denotes componentwise matrix subtraction.

Matrix.nonUnitalNonAssocRing instance

: NonUnitalNonAssocRing (Matrix n n α)

Full source

instance nonUnitalNonAssocRing : NonUnitalNonAssocRing (Matrix n n α) :=
  { Matrix.nonUnitalNonAssocSemiring, Matrix.addCommGroup with }

Square Matrices Form a Non-Unital Non-Associative Ring

Informal description

For any type $n$ and any type $\alpha$ with a non-unital non-associative ring structure, the space of square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ forms a non-unital non-associative ring under matrix addition and multiplication.

Matrix.instNonUnitalRing instance

[Fintype n] [NonUnitalRing α] : NonUnitalRing (Matrix n n α)

Full source

instance instNonUnitalRing [Fintype n] [NonUnitalRing α] : NonUnitalRing (Matrix n n α) :=
  { Matrix.nonUnitalSemiring, Matrix.addCommGroup with }

Square Matrices over a Non-Unital Ring Form a Non-Unital Ring

Informal description

For any finite type $n$ and any non-unital ring $\alpha$, the space of square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ forms a non-unital ring under matrix addition and multiplication.

Matrix.instNonAssocRing instance

[Fintype n] [DecidableEq n] [NonAssocRing α] : NonAssocRing (Matrix n n α)

Full source

instance instNonAssocRing [Fintype n] [DecidableEq n] [NonAssocRing α] :
    NonAssocRing (Matrix n n α) :=
  { Matrix.nonAssocSemiring, Matrix.instAddCommGroupWithOne with }

Square Matrices Form a Non-Associative Ring

Informal description

For any finite type $n$ with decidable equality and any non-associative ring $\alpha$, the square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ form a non-associative ring under matrix addition and multiplication. The operations are defined as follows: - Addition is componentwise and forms an additive commutative group. - Multiplication is given by standard matrix multiplication: $(A * B)_{i,j} = \sum_k A_{i,k} \cdot B_{k,j}$. - The multiplication is distributive over addition and has a multiplicative identity given by the identity matrix (with ones on the diagonal and zeros elsewhere).

Matrix.instRing instance

[Fintype n] [DecidableEq n] [Ring α] : Ring (Matrix n n α)

Full source

instance instRing [Fintype n] [DecidableEq n] [Ring α] : Ring (Matrix n n α) :=
  { Matrix.semiring, Matrix.instAddCommGroupWithOne with }

Square Matrices Form a Ring

Informal description

For any finite type $n$ with decidable equality and any ring $\alpha$, the square matrices $\mathrm{Matrix}\, n\, n\, \alpha$ form a ring under matrix addition and multiplication. The operations are defined as follows: - Addition is componentwise and forms an additive commutative group. - Multiplication is given by standard matrix multiplication: $(A * B)_{i,j} = \sum_k A_{i,k} \cdot B_{k,j}$. - The multiplication is associative, distributive over addition, and has a multiplicative identity given by the identity matrix (with ones on the diagonal and zeros elsewhere).

Matrix.mul_mul_left theorem

[Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) : (of fun i j => a * M i j) * N = a • (M * N)

Full source

@[simp]
theorem mul_mul_left [Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) :
    (of fun i j => a * M i j) * N = a • (M * N) :=
  smul_mul a M N

Left scalar multiplication commutes with matrix multiplication: $(a \cdot M) * N = a \cdot (M * N)$

Informal description

Let $m$, $n$, and $o$ be finite types, and let $\alpha$ be a type with multiplication and an additive commutative monoid structure. For any matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$, matrix $N \in \mathrm{Matrix}\, n\, o\, \alpha$, and scalar $a \in \alpha$, the product of the matrix $(a \cdot M_{ij})_{i,j}$ with $N$ is equal to the scalar multiple $a \cdot (M * N)$, i.e., $$(a \cdot M) * N = a \cdot (M * N).$$

Matrix.smul_eq_mul_diagonal theorem

[Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) : a • M = M * diagonal fun _ => a

Full source

theorem smul_eq_mul_diagonal [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) :
    a • M = M * diagonal fun _ => a := by
  ext
  simp [mul_comm]

Scalar Multiplication as Right Multiplication by Diagonal Matrix: $a \cdot M = M \cdot \text{diag}(a)$

Informal description

Let $m$ and $n$ be finite types with decidable equality, and let $\alpha$ be a type with multiplication and an additive commutative monoid structure. For any matrix $M \in \text{Matrix}\, m\, n\, \alpha$ and scalar $a \in \alpha$, the scalar multiple $a \cdot M$ is equal to the matrix product of $M$ with the diagonal matrix where all diagonal entries are $a$, i.e., $$ a \cdot M = M \cdot \text{diag}(a, \dots, a). $$

Matrix.mul_mul_right theorem

[Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) : (M * of fun i j => a * N i j) = a • (M * N)

Full source

@[simp]
theorem mul_mul_right [Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) :
    (M * of fun i j => a * N i j) = a • (M * N) :=
  mul_smul M a N

Right scalar multiplication commutes with matrix multiplication: $M * (a \cdot N) = a \cdot (M * N)$

Informal description

Let $m$, $n$, and $o$ be types, with $n$ finite. Let $\alpha$ be a type equipped with multiplication and an additive commutative monoid structure. For any matrices $M \in \text{Matrix}\, m\, n\, \alpha$ and $N \in \text{Matrix}\, n\, o\, \alpha$, and any scalar $a \in \alpha$, the matrix product $M * (a \cdot N)$ is equal to $a \cdot (M * N)$, where $a \cdot N$ denotes the matrix obtained by multiplying each entry of $N$ by $a$.

Matrix.vecMulVec definition

[Mul α] (w : m → α) (v : n → α) : Matrix m n α

Full source

/-- For two vectors `w` and `v`, `vecMulVec w v i j` is defined to be `w i * v j`.
    Put another way, `vecMulVec w v` is exactly `col w * row v`. -/
def vecMulVec [Mul α] (w : m → α) (v : n → α) : Matrix m n α :=
  of fun x y => w x * v y

Outer product of two vectors

Informal description

Given two vectors $ w : m \to \alpha $ and $ v : n \to \alpha $ in a type $ \alpha $ equipped with multiplication, the function `Matrix.vecMulVec w v` constructs an $ m \times n $ matrix whose entry at position $(i, j)$ is the product $ w_i \cdot v_j $. This operation is equivalent to the matrix product of the column vector formed from $ w $ and the row vector formed from $ v $.

Matrix.vecMulVec_apply theorem

[Mul α] (w : m → α) (v : n → α) (i j) : vecMulVec w v i j = w i * v j

Full source

theorem vecMulVec_apply [Mul α] (w : m → α) (v : n → α) (i j) : vecMulVec w v i j = w i * v j :=
  rfl

Entry-wise Formula for Outer Product Matrix: $(\text{vecMulVec}(w, v))_{i,j} = w_i \cdot v_j$

Informal description

For any type $\alpha$ equipped with a multiplication operation, and for any vectors $w : m \to \alpha$ and $v : n \to \alpha$, the $(i,j)$-th entry of the outer product matrix $\text{vecMulVec}(w, v)$ is given by the product $w_i \cdot v_j$.

Matrix.mulVec definition

[Fintype n] (M : Matrix m n α) (v : n → α) : m → α

Full source

/--
`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)`.
-/
def mulVec [Fintype n] (M : Matrix m n α) (v : n → α) : m → α
  | i => (fun j => M i j) ⬝ᵥ v

Matrix-vector multiplication

Informal description

Given a finite type `n`, a matrix $M$ of size $m \times n$ with entries in $\alpha$, and a vector $v$ of size $n$ with entries in $\alpha$, the matrix-vector product $M \cdot v$ is the vector of size $m$ whose $i$-th entry is the dot product of the $i$-th row of $M$ with $v$.

Matrix.term_*ᵥ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
scoped infixr:73 " *ᵥ " => Matrix.mulVec

Matrix-vector multiplication notation

Informal description

The infix notation `*ᵥ` with right associativity and precedence level 73 is defined as the matrix-vector multiplication operation `Matrix.mulVec`. Given a matrix $M$ of size $m \times n$ and a vector $v$ of size $n$, the operation $M *ᵥ v$ computes the matrix-vector product resulting in a vector of size $m$.

Matrix.vecMul definition

[Fintype m] (v : m → α) (M : Matrix m n α) : n → α

Full source

/--
`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)`.
-/
def vecMul [Fintype m] (v : m → α) (M : Matrix m n α) : n → α
  | j => v ⬝ᵥ fun i => M i j

Vector-matrix multiplication

Informal description

Given a finite type `m`, a vector `v : m → α`, and a matrix `M : Matrix m n α`, the vector-matrix product `v ᵥ* M` is the vector of type `n → α` whose `j`-th component is the dot product of `v` with the `j`-th column of `M`. In other words, for each column index `j`, the product is computed as $\sum_{i} v_i \cdot M_{i,j}$.

Matrix.term_ᵥ*_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
scoped infixl:73 " ᵥ* " => Matrix.vecMul

Vector-matrix multiplication notation

Informal description

The notation `v ᵥ* M` represents the multiplication of a vector `v` with a matrix `M`, where `v` is a row vector of size `m` and `M` is an `m × n` matrix, resulting in a row vector of size `n`.

Matrix.mulVec.addMonoidHomLeft definition

[Fintype n] (v : n → α) : Matrix m n α →+ m → α

Full source

/-- Left multiplication by a matrix, as an `AddMonoidHom` from vectors to vectors. -/
@[simps]
def mulVec.addMonoidHomLeft [Fintype n] (v : n → α) : MatrixMatrix m n α →+ m → α where
  toFun M := M *ᵥ v
  map_zero' := by
    ext
    simp [mulVec]
  map_add' x y := by
    ext m
    apply add_dotProduct

Matrix-vector multiplication as additive monoid homomorphism

Informal description

For a finite type `n` and a vector `v : n → α`, the function that left-multiplies a matrix `M : Matrix m n α` by `v` is an additive monoid homomorphism from matrices to vectors. More precisely, this defines the map `M ↦ M *ᵥ v` (matrix-vector multiplication) and shows: 1. The zero matrix maps to the zero vector: `0 *ᵥ v = 0` 2. The map preserves addition: `(M + N) *ᵥ v = M *ᵥ v + N *ᵥ v` for any matrices `M, N`

Matrix.mul_apply_eq_vecMul theorem

[Fintype n] (A : Matrix m n α) (B : Matrix n o α) (i : m) : (A * B) i = A i ᵥ* B

Full source

/-- The `i`th row of the multiplication is the same as the `vecMul` with the `i`th row of `A`. -/
theorem mul_apply_eq_vecMul [Fintype n] (A : Matrix m n α) (B : Matrix n o α) (i : m) :
    (A * B) i = A i ᵥ* B :=
  rfl

Row of Matrix Product Equals Vector-Matrix Product of Row

Informal description

For matrices $A \in \mathrm{Matrix}\, m\, n\, \alpha$ and $B \in \mathrm{Matrix}\, n\, o\, \alpha$ over a finite type $n$, the $i$-th row of the matrix product $A * B$ is equal to the vector-matrix product of the $i$-th row of $A$ with $B$, i.e., $(A * B)_i = A_i \cdot B$.

Matrix.vecMul_eq_sum theorem

[Fintype m] (v : m → α) (M : Matrix m n α) : v ᵥ* M = ∑ i, v i • M i

Full source

theorem vecMul_eq_sum [Fintype m] (v : m → α) (M : Matrix m n α) : v ᵥ* M = ∑ i, v i • M i :=
  (Finset.sum_fn ..).symm

Vector-Matrix Product as Sum of Scalar Multiples of Rows

Informal description

For a finite type $m$, a vector $v \colon m \to \alpha$, and a matrix $M \colon \text{Matrix}\, m\, n\, \alpha$, the vector-matrix product $v \text{ ᵥ*} M$ is equal to the sum $\sum_{i \in m} v_i \cdot M_i$, where $M_i$ denotes the $i$-th row of $M$ and $\cdot$ represents scalar multiplication.

Matrix.mulVec_eq_sum theorem

[Fintype n] (v : n → α) (M : Matrix m n α) : M *ᵥ v = ∑ i, MulOpposite.op (v i) • Mᵀ i

Full source

theorem mulVec_eq_sum [Fintype n] (v : n → α) (M : Matrix m n α) :
    M *ᵥ v = ∑ i, MulOpposite.op (v i) • Mᵀ i :=
  (Finset.sum_fn ..).symm

Matrix-Vector Product as Sum of Scalar Multiples of Transposed Rows

Informal description

For a finite type $n$, a vector $v \colon n \to \alpha$, and a matrix $M \colon \text{Matrix}\, m\, n\, \alpha$, the matrix-vector product $M \cdot v$ is equal to the sum $\sum_{i \in n} \text{op}(v_i) \cdot M^\top_i$, where $\text{op}$ denotes the canonical embedding into the multiplicative opposite and $M^\top_i$ is the $i$-th row of the transpose of $M$.

Matrix.mulVec_diagonal theorem

[Fintype m] [DecidableEq m] (v w : m → α) (x : m) : (diagonal v *ᵥ w) x = v x * w x

Full source

theorem mulVec_diagonal [Fintype m] [DecidableEq m] (v w : m → α) (x : m) :
    (diagonaldiagonal v *ᵥ w) x = v x * w x :=
  diagonal_dotProduct v w x

Diagonal Matrix-Vector Product: $(\text{diag}(v) \cdot w)_x = v_x w_x$

Informal description

For any finite type $m$ with decidable equality, and for any vectors $v, w : m \to \alpha$, the matrix-vector product of the diagonal matrix constructed from $v$ with $w$ satisfies $( \text{diag}(v) \cdot w )_x = v_x w_x$ for every index $x \in m$.

Matrix.vecMul_diagonal theorem

[Fintype m] [DecidableEq m] (v w : m → α) (x : m) : (v ᵥ* diagonal w) x = v x * w x

Full source

theorem vecMul_diagonal [Fintype m] [DecidableEq m] (v w : m → α) (x : m) :
    (v ᵥ* diagonal w) x = v x * w x :=
  dotProduct_diagonal' v w x

Vector-Diagonal Matrix Product: $(v \cdot \text{diag}(w))_x = v_x w_x$

Informal description

For any finite type $m$ with decidable equality, and for any vectors $v, w : m \to \alpha$, the vector-matrix product of $v$ with the diagonal matrix constructed from $w$ satisfies $(v \cdot \text{diag}(w))_x = v_x w_x$ for every index $x \in m$.

Matrix.dotProduct_mulVec theorem

 [Fintype n] [Fintype m] [NonUnitalSemiring R] (v : m → R) (A : Matrix m n R) (w : n → R) : v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w

Full source

/-- Associate the dot product of `mulVec` to the left. -/
theorem dotProduct_mulVec [Fintype n] [Fintype m] [NonUnitalSemiring R] (v : m → R)
    (A : Matrix m n R) (w : n → R) : v ⬝ᵥ A *ᵥ w = v ᵥ* Av ᵥ* A ⬝ᵥ w := by
  simp only [dotProduct, vecMul, mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc]
  exact Finset.sum_comm

Associativity of Dot Product with Matrix-Vector Multiplication: $v \cdot (A \cdot w) = (v \cdot A) \cdot w$

Informal description

For any finite types $m$ and $n$, and any non-unital semiring $R$, given vectors $v : m \to R$, $w : n \to R$, and a matrix $A : \text{Matrix } m n R$, the dot product of $v$ with the matrix-vector product $A \cdot w$ equals the dot product of the vector-matrix product $v \cdot A$ with $w$. That is, $$ v \cdot (A \cdot w) = (v \cdot A) \cdot w. $$

Matrix.mulVec_zero theorem

[Fintype n] (A : Matrix m n α) : A *ᵥ 0 = 0

Full source

@[simp]
theorem mulVec_zero [Fintype n] (A : Matrix m n α) : A *ᵥ 0 = 0 := by
  ext
  simp [mulVec]

Matrix-Vector Multiplication with Zero Vector Yields Zero Vector

Informal description

For any finite type `n` and any matrix $A$ of size $m \times n$ with entries in a type $\alpha$, the matrix-vector product of $A$ with the zero vector is the zero vector, i.e., $A \cdot \mathbf{0} = \mathbf{0}$.

Matrix.zero_vecMul theorem

[Fintype m] (A : Matrix m n α) : 0 ᵥ* A = 0

Full source

@[simp]
theorem zero_vecMul [Fintype m] (A : Matrix m n α) : 0 ᵥ* A = 0 := by
  ext
  simp [vecMul]

Zero vector multiplied by any matrix yields the zero vector

Informal description

For any matrix $A$ of size $m \times n$ with entries in an additive commutative monoid $\alpha$, the product of the zero vector (of length $m$) with $A$ is the zero vector (of length $n$), i.e., $0 \cdot A = 0$.

Matrix.zero_mulVec theorem

[Fintype n] (v : n → α) : (0 : Matrix m n α) *ᵥ v = 0

Full source

@[simp]
theorem zero_mulVec [Fintype n] (v : n → α) : (0 : Matrix m n α) *ᵥ v = 0 := by
  ext
  simp [mulVec]

Zero Matrix-Vector Multiplication Yields Zero Vector

Informal description

For any finite type `n` and any vector $v : n \to \alpha$, the matrix-vector product of the zero matrix (of size $m \times n$) with $v$ is the zero vector, i.e., $0 \cdot v = 0$.

Matrix.vecMul_zero theorem

[Fintype m] (v : m → α) : v ᵥ* (0 : Matrix m n α) = 0

Full source

@[simp]
theorem vecMul_zero [Fintype m] (v : m → α) : v ᵥ* (0 : Matrix m n α) = 0 := by
  ext
  simp [vecMul]

Vector-Matrix Product with Zero Matrix Yields Zero Vector

Informal description

For any vector $v : m \to \alpha$ and the zero matrix $0 : \mathrm{Matrix}\, m\, n\, \alpha$, the vector-matrix product $v \cdot 0$ is the zero vector, i.e., $v \cdot 0 = 0$.

Matrix.smul_mulVec_assoc theorem

 [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] (a : R) (A : Matrix m n α) (b : n → α) :
  (a • A) *ᵥ b = a • A *ᵥ b

Full source

theorem smul_mulVec_assoc [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α]
    (a : R) (A : Matrix m n α) (b : n → α) : (a • A) *ᵥ b = a • A *ᵥ b := by
  ext
  apply smul_dotProduct

Associativity of Scalar Multiplication with Matrix-Vector Product: $(a \cdot A) \cdot b = a \cdot (A \cdot b)$

Informal description

Let $R$ be a monoid and $\alpha$ be a type equipped with a distributive multiplicative action of $R$ and a scalar multiplication operation satisfying the compatibility condition `IsScalarTower R α α`. For any scalar $a \in R$, any matrix $A$ of size $m \times n$ with entries in $\alpha$, and any vector $b$ of size $n$ with entries in $\alpha$, the matrix-vector product of the scalar multiple $a \cdot A$ with $b$ is equal to the scalar multiple $a$ applied to the matrix-vector product $A \cdot b$, i.e., $$(a \cdot A) \cdot b = a \cdot (A \cdot b).$$

Matrix.mulVec_add theorem

[Fintype n] (A : Matrix m n α) (x y : n → α) : A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y

Full source

theorem mulVec_add [Fintype n] (A : Matrix m n α) (x y : n → α) :
    A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y := by
  ext
  apply dotProduct_add

Distributivity of Matrix-Vector Multiplication over Vector Addition

Informal description

Let $A$ be an $m \times n$ matrix with entries in a type $\alpha$, and let $x, y$ be $n$-dimensional vectors with entries in $\alpha$. If $n$ is a finite type, then the matrix-vector product satisfies the distributive property: \[ A \cdot (x + y) = A \cdot x + A \cdot y \] where $\cdot$ denotes matrix-vector multiplication.

Matrix.add_mulVec theorem

[Fintype n] (A B : Matrix m n α) (x : n → α) : (A + B) *ᵥ x = A *ᵥ x + B *ᵥ x

Full source

theorem add_mulVec [Fintype n] (A B : Matrix m n α) (x : n → α) :
    (A + B) *ᵥ x = A *ᵥ x + B *ᵥ x := by
  ext
  apply add_dotProduct

Linearity of Matrix-Vector Multiplication over Matrix Addition

Informal description

For any finite type `n`, matrices $A, B \in \mathrm{Matrix}\, m\, n\, \alpha$, and vector $x \in n \to \alpha$, the matrix-vector multiplication satisfies the linearity property: \[ (A + B) \cdot x = A \cdot x + B \cdot x \] where $\cdot$ denotes the matrix-vector product.

Matrix.vecMul_add theorem

[Fintype m] (A B : Matrix m n α) (x : m → α) : x ᵥ* (A + B) = x ᵥ* A + x ᵥ* B

Full source

theorem vecMul_add [Fintype m] (A B : Matrix m n α) (x : m → α) :
    x ᵥ* (A + B) = x ᵥ* A + x ᵥ* B := by
  ext
  apply dotProduct_add

Distributivity of Vector-Matrix Multiplication over Matrix Addition

Informal description

For any finite type $m$, matrices $A, B : \mathrm{Matrix}\, m\, n\, \alpha$, and vector $x : m \to \alpha$ in a type $\alpha$ with addition, the vector-matrix multiplication satisfies the distributive property: \[ x \cdot (A + B) = x \cdot A + x \cdot B \] where $\cdot$ denotes the vector-matrix multiplication operation.

Matrix.add_vecMul theorem

[Fintype m] (A : Matrix m n α) (x y : m → α) : (x + y) ᵥ* A = x ᵥ* A + y ᵥ* A

Full source

theorem add_vecMul [Fintype m] (A : Matrix m n α) (x y : m → α) :
    (x + y) ᵥ* A = x ᵥ* A + y ᵥ* A := by
  ext
  apply add_dotProduct

Linearity of Vector-Matrix Multiplication over Vector Addition

Informal description

For any matrix $A : \text{Matrix}\, m\, n\, \alpha$ over a finite type $m$ and any vectors $x, y : m \to \alpha$, the vector-matrix multiplication satisfies the linearity property: \[ (x + y) \cdot A = x \cdot A + y \cdot A \] where $\cdot$ denotes the vector-matrix multiplication operation.

Matrix.vecMul_smul theorem

 [Fintype n] [NonUnitalNonAssocSemiring S] [DistribSMul R S] [IsScalarTower R S S] (M : Matrix n m S) (b : R)
  (v : n → S) : (b • v) ᵥ* M = b • v ᵥ* M

Full source

theorem vecMul_smul [Fintype n] [NonUnitalNonAssocSemiring S] [DistribSMul R S]
    [IsScalarTower R S S] (M : Matrix n m S) (b : R) (v : n → S) :
    (b • v) ᵥ* M = b • v ᵥ* M := by
  ext i
  simp only [vecMul, dotProduct, Finset.smul_sum, Pi.smul_apply, smul_mul_assoc]

Scalar multiplication commutes with vector-matrix multiplication

Informal description

Let $R$ and $S$ be types with $S$ forming a non-unital non-associative semiring, and suppose $R$ has a distributive scalar multiplication action on $S$ that is compatible via `IsScalarTower`. For a finite type $n$, a matrix $M : \text{Matrix } n \, m \, S$, a scalar $b : R$, and a vector $v : n \to S$, the vector-matrix product satisfies: $$(b \cdot v) \cdot M = b \cdot (v \cdot M)$$ where $\cdot$ denotes the scalar multiplication and vector-matrix multiplication respectively.

Matrix.mulVec_smul theorem

 [Fintype n] [NonUnitalNonAssocSemiring S] [DistribSMul R S] [SMulCommClass R S S] (M : Matrix m n S) (b : R)
  (v : n → S) : M *ᵥ (b • v) = b • M *ᵥ v

Full source

theorem mulVec_smul [Fintype n] [NonUnitalNonAssocSemiring S] [DistribSMul R S]
    [SMulCommClass R S S] (M : Matrix m n S) (b : R) (v : n → S) :
    M *ᵥ (b • v) = b • M *ᵥ v := by
  ext i
  simp only [mulVec, dotProduct, Finset.smul_sum, Pi.smul_apply, mul_smul_comm]

Scalar multiplication commutes with matrix-vector multiplication: $M \cdot (b \cdot v) = b \cdot (M \cdot v)$

Informal description

Let $R$ and $S$ be types with a non-unital non-associative semiring structure on $S$, a distributive scalar multiplication of $R$ on $S$, and a scalar commutativity property. For any finite type $n$, matrix $M \in \text{Matrix}(m \times n, S)$, scalar $b \in R$, and vector $v \in n \to S$, the matrix-vector product satisfies: \[ M \cdot (b \cdot v) = b \cdot (M \cdot v) \]

Matrix.mulVec_single theorem

 [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (M : Matrix m n R) (j : n) (x : R) :
  M *ᵥ Pi.single j x = MulOpposite.op x • Mᵀ j

Full source

@[simp]
theorem mulVec_single [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (M : Matrix m n R)
    (j : n) (x : R) : M *ᵥ Pi.single j x = MulOpposite.op x • Mᵀ j :=
  funext fun _ => dotProduct_single _ _ _

Matrix-vector multiplication with a single nonzero entry: $M \cdot \text{single}_j x = \text{op}(x) \cdot M^\top_j$

Informal description

Let $R$ be a non-unital, non-associative semiring, and let $n$ be a finite type with decidable equality. For any matrix $M \in \text{Matrix}(m \times n, R)$, any index $j \in n$, and any element $x \in R$, the matrix-vector product of $M$ with the vector $\text{Pi.single}\ j\ x$ (which is $x$ at index $j$ and $0$ elsewhere) equals the scalar multiple $\text{op}(x) \cdot M^\top_j$, where $M^\top_j$ is the $j$-th column of the transpose of $M$ and $\text{op}(x)$ denotes the multiplicative opposite of $x$ in $R^\text{op}$.

Matrix.single_vecMul theorem

 [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring R] (M : Matrix m n R) (i : m) (x : R) :
  Pi.single i x ᵥ* M = x • M i

Full source

@[simp]
theorem single_vecMul [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring R] (M : Matrix m n R)
    (i : m) (x : R) : Pi.singlePi.single i x ᵥ* M = x • M i :=
  funext fun _ => single_dotProduct _ _ _

Vector-Matrix Multiplication with Single Nonzero Entry: $(\text{single}_i x) \cdot M = x M_i$

Informal description

Let $R$ be a non-unital, non-associative semiring, and let $m$ and $n$ be finite types with decidable equality on $m$. For any matrix $M \in \text{Matrix}(m, n, R)$, any index $i \in m$, and any element $x \in R$, the vector-matrix product of the vector $\text{Pi.single}\ i\ x$ (which is $x$ at index $i$ and $0$ elsewhere) with $M$ equals the scalar multiple $x \cdot M_i$, where $M_i$ denotes the $i$-th row of $M$.

Matrix.mulVec_single_one theorem

[Fintype n] [DecidableEq n] [NonAssocSemiring R] (M : Matrix m n R) (j : n) : M *ᵥ Pi.single j 1 = Mᵀ j

Full source

theorem mulVec_single_one [Fintype n] [DecidableEq n] [NonAssocSemiring R]
    (M : Matrix m n R) (j : n) :
    M *ᵥ Pi.single j 1 = Mᵀ j := by ext; simp

Matrix-vector product with single one entry yields transpose column: $M \cdot \text{single}_j 1 = M^\top_j$

Informal description

Let $R$ be a non-associative semiring, and let $n$ be a finite type with decidable equality. For any matrix $M \in \text{Matrix}(m \times n, R)$ and any index $j \in n$, the matrix-vector product of $M$ with the vector $\text{Pi.single}\ j\ 1$ (which is $1$ at index $j$ and $0$ elsewhere) equals the $j$-th column of the transpose of $M$, i.e., $M \cdot \text{single}_j 1 = M^\top_j$.

Matrix.single_one_vecMul theorem

[Fintype m] [DecidableEq m] [NonAssocSemiring R] (i : m) (M : Matrix m n R) : Pi.single i 1 ᵥ* M = M i

Full source

theorem single_one_vecMul [Fintype m] [DecidableEq m] [NonAssocSemiring R]
    (i : m) (M : Matrix m n R) :
    Pi.singlePi.single i 1 ᵥ* M = M i := by ext; simp

Vector-Matrix Multiplication with Single One Entry Yields Row: $(\text{single}_i 1) \cdot M = M_i$

Informal description

Let $R$ be a non-associative semiring, and let $m$ and $n$ be finite types with decidable equality on $m$. For any matrix $M \in \text{Matrix}(m, n, R)$ and any index $i \in m$, the vector-matrix product of the vector $\text{Pi.single}\ i\ 1$ (which is $1$ at index $i$ and $0$ elsewhere) with $M$ equals the $i$-th row of $M$, i.e., $(\text{single}_i 1) \cdot M = M_i$.

Matrix.diagonal_mulVec_single theorem

 [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R) (j : n) (x : R) :
  diagonal v *ᵥ Pi.single j x = Pi.single j (v j * x)

Full source

theorem diagonal_mulVec_single [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R)
    (j : n) (x : R) : diagonaldiagonal v *ᵥ Pi.single j x = Pi.single j (v j * x) := by
  ext i
  rw [mulVec_diagonal]
  exact Pi.apply_single (fun i x => v i * x) (fun i => mul_zero _) j x i

Diagonal Matrix-Vector Product with Single-Entry Vector: $\text{diag}(v) \cdot \text{single}_j(x) = \text{single}_j(v_j x)$

Informal description

Let $n$ be a finite type with decidable equality and $R$ be a non-unital non-associative semiring. For any vector $v : n \to R$, index $j \in n$, and scalar $x \in R$, the matrix-vector product of the diagonal matrix $\text{diag}(v)$ with the single-entry vector $\text{Pi.single}_j(x)$ equals the single-entry vector $\text{Pi.single}_j(v_j \cdot x)$. In other words, for the vector with $x$ at position $j$ and zeros elsewhere, multiplying it by a diagonal matrix with entries $v$ results in a vector with $v_j \cdot x$ at position $j$ and zeros elsewhere.

Matrix.single_vecMul_diagonal theorem

 [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R) (j : n) (x : R) :
  (Pi.single j x) ᵥ* (diagonal v) = Pi.single j (x * v j)

Full source

theorem single_vecMul_diagonal [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R)
    (j : n) (x : R) : (Pi.single j x) ᵥ* (diagonal v) = Pi.single j (x * v j) := by
  ext i
  rw [vecMul_diagonal]
  exact Pi.apply_single (fun i x => x * v i) (fun i => zero_mul _) j x i

Single-Entry Vector Multiplication with Diagonal Matrix: $(\text{single}_j(x)) \cdot \text{diag}(v) = \text{single}_j(x \cdot v_j)$

Informal description

Let $n$ be a finite type with decidable equality and $R$ be a non-unital non-associative semiring. For any vector $v : n \to R$, index $j \in n$, and scalar $x \in R$, the vector-matrix product of the single-entry vector $\text{Pi.single}_j(x)$ with the diagonal matrix $\text{diag}(v)$ equals the single-entry vector $\text{Pi.single}_j(x \cdot v_j)$. In other words, for the vector with $x$ at position $j$ and zeros elsewhere, multiplying it by a diagonal matrix with entries $v$ results in a vector with $x \cdot v_j$ at position $j$ and zeros elsewhere.

Matrix.vecMul_vecMul theorem

[Fintype n] [Fintype m] (v : m → α) (M : Matrix m n α) (N : Matrix n o α) : v ᵥ* M ᵥ* N = v ᵥ* (M * N)

Full source

@[simp]
theorem vecMul_vecMul [Fintype n] [Fintype m] (v : m → α) (M : Matrix m n α) (N : Matrix n o α) :
    v ᵥ* Mv ᵥ* M ᵥ* N = v ᵥ* (M * N) := by
  ext
  apply dotProduct_assoc

Associativity of Vector-Matrix Multiplication: $v \mathbin{ᵥ*} (M \mathbin{ᵥ*} N) = v \mathbin{ᵥ*} (M * N)$

Informal description

Let $m$, $n$, and $o$ be finite types, and let $\alpha$ be a type with multiplication and an additive commutative monoid structure. For any vector $v : m \to \alpha$ and matrices $M : \text{Matrix}\, m\, n\, \alpha$ and $N : \text{Matrix}\, n\, o\, \alpha$, the following equality holds: \[ v \mathbin{ᵥ*} M \mathbin{ᵥ*} N = v \mathbin{ᵥ*} (M * N). \] Here, $v \mathbin{ᵥ*} M$ denotes the vector-matrix product of $v$ with $M$, and $M * N$ denotes the matrix product of $M$ with $N$.

Matrix.mulVec_mulVec theorem

[Fintype n] [Fintype o] (v : o → α) (M : Matrix m n α) (N : Matrix n o α) : M *ᵥ N *ᵥ v = (M * N) *ᵥ v

Full source

@[simp]
theorem mulVec_mulVec [Fintype n] [Fintype o] (v : o → α) (M : Matrix m n α) (N : Matrix n o α) :
    M *ᵥ N *ᵥ v = (M * N) *ᵥ v := by
  ext
  symm
  apply dotProduct_assoc

Associativity of Matrix-Vector Multiplication: $M \cdot (N \cdot v) = (M \cdot N) \cdot v$

Informal description

Let $m$, $n$, and $o$ be finite types, and let $\alpha$ be a type with appropriate algebraic operations. Given a matrix $M$ of size $m \times n$, a matrix $N$ of size $n \times o$, and a vector $v$ of size $o$, the following equality holds: \[ M \cdot (N \cdot v) = (M \cdot N) \cdot v, \] where $\cdot$ denotes matrix-vector multiplication and matrix multiplication respectively.

Matrix.mul_mul_apply theorem

[Fintype n] (A B C : Matrix n n α) (i j : n) : (A * B * C) i j = A i ⬝ᵥ B *ᵥ (Cᵀ j)

Full source

theorem mul_mul_apply [Fintype n] (A B C : Matrix n n α) (i j : n) :
    (A * B * C) i j = A i ⬝ᵥ B *ᵥ (Cᵀ j) := by
  rw [Matrix.mul_assoc]
  simp only [mul_apply, dotProduct, mulVec]
  rfl

Matrix Triple Product Entry Formula: $(ABC)_{i,j} = A_i \cdot (B \cdot C_j^\top)$

Informal description

Let $n$ be a finite type and let $\alpha$ be a type with multiplication and an additive commutative monoid structure. For any square matrices $A, B, C \in \mathrm{Matrix}\, n\, n\, \alpha$ and indices $i, j \in n$, the $(i,j)$-th entry of the matrix product $A * B * C$ is equal to the dot product of the $i$-th row of $A$ with the vector obtained by multiplying $B$ with the $j$-th column of $C^\top$ (which is the $j$-th row of $C$). In symbols: \[ (A * B * C)_{i,j} = A_i \cdot (B \cdot C_j^\top) \] where $A_i$ denotes the $i$-th row of $A$, $C_j^\top$ denotes the $j$-th row of $C$, and $\cdot$ denotes the dot product and matrix-vector multiplication respectively.

Matrix.mulVec_one theorem

[Fintype n] (A : Matrix m n α) : A *ᵥ 1 = ∑ j, Aᵀ j

Full source

theorem mulVec_one [Fintype n] (A : Matrix m n α) : A *ᵥ 1 = ∑ j, Aᵀ j := by
  ext; simp [mulVec, dotProduct]

Matrix-Vector Product with Ones Vector Equals Column Sum

Informal description

Let $m$ and $n$ be finite types, and let $A$ be an $m \times n$ matrix with entries in a type $\alpha$. Then the matrix-vector product of $A$ with the constant vector $1$ (where all entries are $1$) equals the sum of the columns of $A$, i.e., $$ A \cdot \mathbf{1} = \sum_{j} A^\top_j $$ where $A^\top_j$ denotes the $j$-th column of $A$ (equivalently, the $j$-th row of the transpose matrix $A^\top$).

Matrix.one_vecMul theorem

[Fintype m] (A : Matrix m n α) : 1 ᵥ* A = ∑ i, A i

Full source

theorem one_vecMul [Fintype m] (A : Matrix m n α) : 1 ᵥ* A = ∑ i, A i := by
  ext; simp [vecMul, dotProduct]

Vector-Matrix Product with Constant One Vector Equals Row Sum

Informal description

Let $m$ be a finite type and let $A$ be an $m \times n$ matrix with entries in a type $\alpha$. Then the vector-matrix product of the constant vector $1$ (with all entries equal to $1$) and $A$ is equal to the sum of the rows of $A$, i.e., $$ 1 \mathbin{\text{ᵥ*}} A = \sum_{i} A_i $$ where $A_i$ denotes the $i$-th row of $A$.

Matrix.ext_of_mulVec_single theorem

[DecidableEq n] [Fintype n] {M N : Matrix m n α} (h : ∀ i, M *ᵥ Pi.single i 1 = N *ᵥ Pi.single i 1) : M = N

Full source

lemma ext_of_mulVec_single [DecidableEq n] [Fintype n] {M N : Matrix m n α}
    (h : ∀ i, M *ᵥ Pi.single i 1 = N *ᵥ Pi.single i 1) :
    M = N := by
  ext i j
  simp_rw [mulVec_single_one] at h
  exact congrFun (h j) i

Matrix Equality via Matrix-Vector Multiplication with Standard Basis Vectors: $M \cdot \text{single}_i 1 = N \cdot \text{single}_i 1$ for all $i$ implies $M = N$

Informal description

Let $m$ and $n$ be finite types with decidable equality on $n$, and let $M, N$ be $m \times n$ matrices over a type $\alpha$. If for every index $i \in n$, the matrix-vector product of $M$ with the standard basis vector $\text{single}_i 1$ (which is $1$ at index $i$ and $0$ elsewhere) equals the corresponding product with $N$, then $M = N$.

Matrix.ext_of_single_vecMul theorem

[DecidableEq m] [Fintype m] {M N : Matrix m n α} (h : ∀ i, Pi.single i 1 ᵥ* M = Pi.single i 1 ᵥ* N) : M = N

Full source

lemma ext_of_single_vecMul [DecidableEq m] [Fintype m] {M N : Matrix m n α}
    (h : ∀ i, Pi.singlePi.single i 1 ᵥ* M = Pi.singlePi.single i 1 ᵥ* N) :
    M = N := by
  ext i j
  simp_rw [single_one_vecMul] at h
  exact congrFun (h i) j

Matrix Equality via Vector-Multiplication with Standard Basis Vectors: $(\text{single}_i 1) \cdot M = (\text{single}_i 1) \cdot N$ for all $i$ implies $M = N$

Informal description

Let $m$ and $n$ be finite types with decidable equality on $m$, and let $M, N$ be $m \times n$ matrices over a type $\alpha$. If for every index $i \in m$, the vector-matrix product of the standard basis vector $\text{single}_i 1$ (which is $1$ at index $i$ and $0$ elsewhere) with $M$ equals the corresponding product with $N$, then $M = N$.

Matrix.one_mulVec theorem

(v : m → α) : 1 *ᵥ v = v

Full source

@[simp]
theorem one_mulVec (v : m → α) : 1 *ᵥ v = v := by
  ext
  rw [← diagonal_one, mulVec_diagonal, one_mul]

Left identity property for matrix-vector multiplication: $I \cdot v = v$

Informal description

For any vector $v : m \to \alpha$, the matrix-vector product of the identity matrix $I$ (of size $m \times m$) with $v$ equals $v$, i.e., $I \cdot v = v$.

Matrix.vecMul_one theorem

(v : m → α) : v ᵥ* 1 = v

Full source

@[simp]
theorem vecMul_one (v : m → α) : v ᵥ* 1 = v := by
  ext
  rw [← diagonal_one, vecMul_diagonal, mul_one]

Right identity property for vector-matrix multiplication: $v \cdot I = v$

Informal description

For any vector $v : m \to \alpha$, the vector-matrix product of $v$ with the identity matrix of size $m \times m$ equals $v$, i.e., $v \cdot I = v$.

Matrix.diagonal_const_mulVec theorem

(x : α) (v : m → α) : (diagonal fun _ => x) *ᵥ v = x • v

Full source

@[simp]
theorem diagonal_const_mulVec (x : α) (v : m → α) :
    (diagonal fun _ => x) *ᵥ v = x • v := by
  ext; simp [mulVec_diagonal]

Diagonal Matrix-Vector Product with Constant Diagonal: $\text{diag}(x, \dots, x) \cdot v = x \cdot v$

Informal description

For any scalar $x \in \alpha$ and any vector $v : m \to \alpha$, the matrix-vector product of the diagonal matrix with constant diagonal entries $x$ and the vector $v$ equals the scalar multiplication of $x$ with $v$, i.e., $$(\text{diag}(x, \dots, x) \cdot v)_i = x \cdot v_i \quad \text{for all } i \in m.$$

Matrix.vecMul_diagonal_const theorem

(x : α) (v : m → α) : v ᵥ* (diagonal fun _ => x) = MulOpposite.op x • v

Full source

@[simp]
theorem vecMul_diagonal_const (x : α) (v : m → α) :
    v ᵥ* (diagonal fun _ => x) = MulOpposite.op x • v := by
  ext; simp [vecMul_diagonal]

Vector-Diagonal Matrix Product with Constant Diagonal: $v \cdot \text{diag}(x, \dots, x) = x^{\text{op}} \cdot v$

Informal description

For any scalar $x$ in a type $\alpha$ with a zero element, and any vector $v : m \to \alpha$, the vector-matrix product of $v$ with the diagonal matrix where every diagonal entry is $x$ equals the scalar multiplication of $x$ (in the multiplicative opposite of $\alpha$) with the vector $v$. That is, $v \cdot \text{diag}(x, \dots, x) = x^{\text{op}} \cdot v$.

Matrix.natCast_mulVec theorem

(x : ℕ) (v : m → α) : x *ᵥ v = (x : α) • v

Full source

@[simp]
theorem natCast_mulVec (x : ℕ) (v : m → α) : x *ᵥ v = (x : α) • v :=
  diagonal_const_mulVec _ _

Matrix-Vector Product with Scalar Matrix: $(x I) \cdot v = x \cdot v$

Informal description

For any natural number $x$ and vector $v : m \to \alpha$, the matrix-vector product of the scalar matrix $x I$ (where $I$ is the identity matrix) with $v$ equals the scalar multiplication of $x$ (as an element of $\alpha$) with $v$, i.e., $$(x I) \cdot v = x \cdot v.$$

Matrix.vecMul_natCast theorem

(x : ℕ) (v : m → α) : v ᵥ* x = MulOpposite.op (x : α) • v

Full source

@[simp]
theorem vecMul_natCast (x : ℕ) (v : m → α) : v ᵥ* x = MulOpposite.op (x : α) • v :=
  vecMul_diagonal_const _ _

Vector-matrix product with scalar matrix: $v \cdot (x I) = x^{\text{op}} \cdot v$

Informal description

For any natural number $x$ and vector $v : m \to \alpha$, the vector-matrix product of $v$ with the scalar matrix $x I$ (where $I$ is the identity matrix) equals the scalar multiplication of $x^{\text{op}}$ (the multiplicative opposite of $x$ in $\alpha$) with the vector $v$. That is, $v \cdot (x I) = x^{\text{op}} \cdot v$.

Matrix.ofNat_mulVec theorem

(x : ℕ) [x.AtLeastTwo] (v : m → α) : ofNat(x) *ᵥ v = (OfNat.ofNat x : α) • v

Full source

@[simp]
theorem ofNat_mulVec (x : ℕ) [x.AtLeastTwo] (v : m → α) :
    ofNat(x)ofNat(x) *ᵥ v = (OfNat.ofNat x : α) • v :=
  natCast_mulVec _ _

Matrix-vector product with scalar matrix: $(x I) \cdot v = x \cdot v$ for $x \geq 2$

Informal description

For any natural number $x \geq 2$ and vector $v : m \to \alpha$, the matrix-vector product of the scalar matrix $x I$ (where $I$ is the identity matrix) with $v$ equals the scalar multiplication of $x$ (as an element of $\alpha$) with $v$, i.e., $$(x I) \cdot v = x \cdot v.$$

Matrix.vecMul_ofNat theorem

(x : ℕ) [x.AtLeastTwo] (v : m → α) : v ᵥ* ofNat(x) = MulOpposite.op (OfNat.ofNat x : α) • v

Full source

@[simp]
theorem vecMul_ofNat (x : ℕ) [x.AtLeastTwo] (v : m → α) :
    v ᵥ* ofNat(x) = MulOpposite.op (OfNat.ofNat x : α) • v :=
  vecMul_natCast _ _

Vector-matrix product with scalar matrix: $v \cdot (x I) = x^{\text{op}} \cdot v$ for $x \geq 2$

Informal description

For any natural number $x \geq 2$ and vector $v : m \to \alpha$, the vector-matrix product of $v$ with the scalar matrix $x I$ (where $I$ is the identity matrix) equals the scalar multiplication of $x^{\text{op}}$ (the multiplicative opposite of $x$ in $\alpha$) with the vector $v$. That is, $v \cdot (x I) = x^{\text{op}} \cdot v$.

Matrix.neg_vecMul theorem

[Fintype m] (v : m → α) (A : Matrix m n α) : (-v) ᵥ* A = -(v ᵥ* A)

Full source

theorem neg_vecMul [Fintype m] (v : m → α) (A : Matrix m n α) : (-v) ᵥ* A = - (v ᵥ* A) := by
  ext
  apply neg_dotProduct

Negation and Vector-Matrix Multiplication: $(-v) \cdot A = -(v \cdot A)$

Informal description

For a finite type $m$, a vector $v : m \to \alpha$, and a matrix $A : \text{Matrix}\, m\, n\, \alpha$, the vector-matrix product of the negated vector $-v$ with $A$ equals the negation of the vector-matrix product of $v$ with $A$, i.e., $(-v) \cdot A = -(v \cdot A)$.

Matrix.vecMul_neg theorem

[Fintype m] (v : m → α) (A : Matrix m n α) : v ᵥ* (-A) = -(v ᵥ* A)

Full source

theorem vecMul_neg [Fintype m] (v : m → α) (A : Matrix m n α) : v ᵥ* (-A) = - (v ᵥ* A) := by
  ext
  apply dotProduct_neg

Negation of Matrix in Vector-Matrix Product: $v \cdot (-A) = -(v \cdot A)$

Informal description

For a finite type `m`, a vector `v : m → α`, and a matrix `A : Matrix m n α`, the vector-matrix product of `v` with the negation of `A` equals the negation of the vector-matrix product of `v` with `A`, i.e., $v \cdot (-A) = -(v \cdot A)$.

Matrix.neg_vecMul_neg theorem

[Fintype m] (v : m → α) (A : Matrix m n α) : (-v) ᵥ* (-A) = v ᵥ* A

Full source

lemma neg_vecMul_neg [Fintype m] (v : m → α) (A : Matrix m n α) : (-v) ᵥ* (-A) = v ᵥ* A := by
  rw [vecMul_neg, neg_vecMul, neg_neg]

Double Negation in Vector-Matrix Product: $(-v) \cdot (-A) = v \cdot A$

Informal description

For a finite type $m$, a vector $v : m \to \alpha$, and a matrix $A : \text{Matrix}\, m\, n\, \alpha$, the vector-matrix product of the negated vector $-v$ with the negated matrix $-A$ equals the original vector-matrix product $v \cdot A$, i.e., $(-v) \cdot (-A) = v \cdot A$.

Matrix.neg_mulVec theorem

[Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ v = -(A *ᵥ v)

Full source

theorem neg_mulVec [Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ v = - (A *ᵥ v) := by
  ext
  apply neg_dotProduct

Negation and Matrix-Vector Multiplication: $(-A) \cdot v = -(A \cdot v)$

Informal description

For a finite type `n`, a vector $v : n \to \alpha$, and a matrix $A : \text{Matrix}\, m\, n\, \alpha$, the matrix-vector product of $-A$ with $v$ equals the negation of the matrix-vector product of $A$ with $v$, i.e., $(-A) \cdot v = -(A \cdot v)$.

Matrix.mulVec_neg theorem

[Fintype n] (v : n → α) (A : Matrix m n α) : A *ᵥ (-v) = -(A *ᵥ v)

Full source

theorem mulVec_neg [Fintype n] (v : n → α) (A : Matrix m n α) : A *ᵥ (-v) = - (A *ᵥ v) := by
  ext
  apply dotProduct_neg

Matrix-Vector Product with Negated Vector: $A \cdot (-v) = -(A \cdot v)$

Informal description

For a finite type `n`, a vector $v : n \to \alpha$, and a matrix $A : \text{Matrix}\, m\, n\, \alpha$, the matrix-vector product of $A$ with $-v$ equals the negation of the matrix-vector product of $A$ with $v$, i.e., $A \cdot (-v) = -(A \cdot v)$.

Matrix.neg_mulVec_neg theorem

[Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ (-v) = A *ᵥ v

Full source

lemma neg_mulVec_neg [Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ (-v) = A *ᵥ v := by
  rw [mulVec_neg, neg_mulVec, neg_neg]

Double Negation in Matrix-Vector Multiplication: $(-A) \cdot (-v) = A \cdot v$

Informal description

For a finite type `n`, a vector $v : n \to \alpha$, and a matrix $A : \text{Matrix}\, m\, n\, \alpha$, the matrix-vector product of $-A$ with $-v$ equals the matrix-vector product of $A$ with $v$, i.e., $(-A) \cdot (-v) = A \cdot v$.

Matrix.mulVec_sub theorem

[Fintype n] (A : Matrix m n α) (x y : n → α) : A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y

Full source

theorem mulVec_sub [Fintype n] (A : Matrix m n α) (x y : n → α) :
    A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y := by
  ext
  apply dotProduct_sub

Matrix-Vector Multiplication Distributes over Vector Subtraction: $A \cdot (x - y) = A \cdot x - A \cdot y$

Informal description

For a finite type `n`, a matrix $A : \text{Matrix}\, m\, n\, \alpha$, and vectors $x, y : n \to \alpha$, the matrix-vector product satisfies the linearity property with respect to vector subtraction: \[ A \cdot (x - y) = A \cdot x - A \cdot y \] where $\cdot$ denotes the matrix-vector multiplication operation.

Matrix.sub_mulVec theorem

[Fintype n] (A B : Matrix m n α) (x : n → α) : (A - B) *ᵥ x = A *ᵥ x - B *ᵥ x

Full source

theorem sub_mulVec [Fintype n] (A B : Matrix m n α) (x : n → α) :
    (A - B) *ᵥ x = A *ᵥ x - B *ᵥ x := by simp [sub_eq_add_neg, add_mulVec, neg_mulVec]

Linearity of Matrix-Vector Multiplication over Matrix Subtraction

Informal description

For any finite type $n$, matrices $A, B \in \mathrm{Matrix}\, m\, n\, \alpha$, and vector $x \in n \to \alpha$, the matrix-vector multiplication satisfies: \[ (A - B) \cdot x = A \cdot x - B \cdot x \] where $\cdot$ denotes the matrix-vector product.

Matrix.vecMul_sub theorem

[Fintype m] (A B : Matrix m n α) (x : m → α) : x ᵥ* (A - B) = x ᵥ* A - x ᵥ* B

Full source

theorem vecMul_sub [Fintype m] (A B : Matrix m n α) (x : m → α) :
    x ᵥ* (A - B) = x ᵥ* A - x ᵥ* B := by simp [sub_eq_add_neg, vecMul_add, vecMul_neg]

Distributivity of Vector-Matrix Multiplication over Matrix Subtraction: $x \cdot (A - B) = x \cdot A - x \cdot B$

Informal description

For any finite type $m$, matrices $A, B \in \mathrm{Matrix}\, m\, n\, \alpha$, and vector $x \in \alpha^m$, the vector-matrix product satisfies: \[ x \cdot (A - B) = x \cdot A - x \cdot B \] where $\cdot$ denotes the vector-matrix multiplication operation.

Matrix.sub_vecMul theorem

[Fintype m] (A : Matrix m n α) (x y : m → α) : (x - y) ᵥ* A = x ᵥ* A - y ᵥ* A

Full source

theorem sub_vecMul [Fintype m] (A : Matrix m n α) (x y : m → α) :
    (x - y) ᵥ* A = x ᵥ* A - y ᵥ* A := by
  ext
  apply sub_dotProduct

Linearity of Vector-Matrix Multiplication over Vector Subtraction

Informal description

Let $m$ be a finite type, $A$ be an $m \times n$ matrix with entries in a type $\alpha$, and $x, y$ be vectors in $\alpha^m$. Then the vector-matrix product of the difference $x - y$ with $A$ equals the difference of the vector-matrix products: $$ (x - y) \cdot A = x \cdot A - y \cdot A. $$

Matrix.mulVec_transpose theorem

[Fintype m] (A : Matrix m n α) (x : m → α) : Aᵀ *ᵥ x = x ᵥ* A

Full source

theorem mulVec_transpose [Fintype m] (A : Matrix m n α) (x : m → α) : AᵀAᵀ *ᵥ x = x ᵥ* A := by
  ext
  apply dotProduct_comm

Transpose Matrix-Vector Product Equals Vector-Matrix Product

Informal description

Let $m$ be a finite type, $A$ be an $m \times n$ matrix with entries in $\alpha$, and $x$ be a vector in $\alpha^m$. Then the matrix-vector product of the transpose $A^\top$ with $x$ equals the vector-matrix product of $x$ with $A$, i.e., $$ A^\top \cdot x = x \cdot A. $$

Matrix.vecMul_transpose theorem

[Fintype n] (A : Matrix m n α) (x : n → α) : x ᵥ* Aᵀ = A *ᵥ x

Full source

theorem vecMul_transpose [Fintype n] (A : Matrix m n α) (x : n → α) : x ᵥ* Aᵀ = A *ᵥ x := by
  ext
  apply dotProduct_comm

Equivalence of Vector-Matrix Multiplication with Transpose and Matrix-Vector Multiplication

Informal description

Let $m$ and $n$ be finite types, $A$ be an $m \times n$ matrix with entries in $\alpha$, and $x$ be a vector in $n \to \alpha$. Then the vector-matrix product of $x$ with the transpose $A^\top$ equals the matrix-vector product of $A$ with $x$, i.e., $x \cdot A^\top = A \cdot x$.

Matrix.mulVec_vecMul theorem

[Fintype n] [Fintype o] (A : Matrix m n α) (B : Matrix o n α) (x : o → α) : A *ᵥ (x ᵥ* B) = (A * Bᵀ) *ᵥ x

Full source

theorem mulVec_vecMul [Fintype n] [Fintype o] (A : Matrix m n α) (B : Matrix o n α) (x : o → α) :
    A *ᵥ (x ᵥ* B) = (A * Bᵀ) *ᵥ x := by rw [← mulVec_mulVec, mulVec_transpose]

Matrix-Vector Multiplication Identity: $A \cdot (x \cdot B) = (A \cdot B^\top) \cdot x$

Informal description

Let $m$, $n$, and $o$ be finite types, and let $\alpha$ be a type with appropriate algebraic operations. Given matrices $A \in \mathrm{Matrix}\, m\, n\, \alpha$ and $B \in \mathrm{Matrix}\, o\, n\, \alpha$, and a vector $x \in o \to \alpha$, the following equality holds: \[ A \cdot (x \cdot B) = (A \cdot B^\top) \cdot x, \] where $\cdot$ denotes matrix-vector multiplication, vector-matrix multiplication, and matrix multiplication respectively, and $B^\top$ is the transpose of $B$.

Matrix.vecMul_mulVec theorem

[Fintype m] [Fintype n] (A : Matrix m n α) (B : Matrix m o α) (x : n → α) : (A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B)

Full source

theorem vecMul_mulVec [Fintype m] [Fintype n] (A : Matrix m n α) (B : Matrix m o α) (x : n → α) :
    (A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B) := by rw [← vecMul_vecMul, vecMul_transpose]

Vector-Matrix and Matrix-Vector Multiplication Identity: $(A \cdot x) \cdot B = x \cdot (A^\top \cdot B)$

Informal description

Let $m$, $n$, and $o$ be finite types, and let $\alpha$ be a type with multiplication and an additive commutative monoid structure. For any matrices $A \in \text{Matrix}\, m\, n\, \alpha$ and $B \in \text{Matrix}\, m\, o\, \alpha$, and any vector $x \in n \to \alpha$, the following equality holds: \[ (A \cdot x) \cdot B = x \cdot (A^\top \cdot B). \] Here, $A \cdot x$ denotes the matrix-vector product of $A$ with $x$, $x \cdot (A^\top \cdot B)$ denotes the vector-matrix product of $x$ with the matrix product of $A^\top$ and $B$, and $A^\top$ is the transpose of $A$.

Matrix.mulVec_injective_of_isUnit theorem

[Fintype m] [DecidableEq m] {A : Matrix m m R} (ha : IsUnit A) : Function.Injective A.mulVec

Full source

lemma mulVec_injective_of_isUnit [Fintype m] [DecidableEq m] {A : Matrix m m R}
    (ha : IsUnit A) : Function.Injective A.mulVec := by
  obtain ⟨B, hBl, hBr⟩ := isUnit_iff_exists.mp ha
  intro x y hxy
  simpa [hBr] using congrArg B.mulVec hxy

Injectivity of Matrix-Vector Multiplication for Invertible Matrices

Informal description

Let $m$ be a finite type with decidable equality, and let $R$ be a type with appropriate algebraic operations. For any square matrix $A \in \mathrm{Matrix}\, m\, m\, R$ that is a unit (i.e., invertible), the matrix-vector multiplication map $A \cdot \_ : (m \to R) \to (m \to R)$ is injective.

Matrix.vecMul_injective_of_isUnit theorem

[Fintype m] [DecidableEq m] {A : Matrix m m R} (ha : IsUnit A) : Function.Injective A.vecMul

Full source

lemma vecMul_injective_of_isUnit [Fintype m] [DecidableEq m] {A : Matrix m m R}
    (ha : IsUnit A) : Function.Injective A.vecMul := by
  obtain ⟨B, hBl, hBr⟩ := isUnit_iff_exists.mp ha
  intro x y hxy
  simpa [hBl] using congrArg B.vecMul hxy

Injectivity of Vector-Matrix Multiplication by an Invertible Matrix

Informal description

Let $m$ be a finite type with decidable equality, and let $R$ be a type with a monoid structure. For any square matrix $A \in \mathrm{Matrix}\, m\, m\, R$ that is a unit (i.e., invertible), the vector-matrix multiplication map $v \mapsto v \mathbin{ᵥ*} A$ is injective. In other words, if $v \mathbin{ᵥ*} A = w \mathbin{ᵥ*} A$ for vectors $v, w \in m \to R$, then $v = w$.

Matrix.mulVec_smul_assoc theorem

[Fintype n] (A : Matrix m n α) (b : n → α) (a : α) : A *ᵥ (a • b) = a • A *ᵥ b

Full source

theorem mulVec_smul_assoc [Fintype n] (A : Matrix m n α) (b : n → α) (a : α) :
    A *ᵥ (a • b) = a • A *ᵥ b := by
  ext
  apply dotProduct_smul

Associativity of Matrix-Vector Multiplication with Scalar Multiplication: $A \cdot (a \cdot b) = a \cdot (A \cdot b)$

Informal description

Let $m$ and $n$ be finite types, and let $\alpha$ be a type with a scalar multiplication operation. For any matrix $A : \text{Matrix}\, m\, n\, \alpha$, vector $b : n \to \alpha$, and scalar $a : \alpha$, the matrix-vector product of $A$ with the scaled vector $a \cdot b$ is equal to the scalar $a$ multiplied by the matrix-vector product of $A$ with $b$, i.e., $$ A \cdot (a \cdot b) = a \cdot (A \cdot b). $$

Matrix.intCast_mulVec theorem

(x : ℤ) (v : m → α) : x *ᵥ v = (x : α) • v

Full source

@[simp]
theorem intCast_mulVec (x : ℤ) (v : m → α) : x *ᵥ v = (x : α) • v :=
  diagonal_const_mulVec _ _

Scalar-Vector Multiplication via Integer Cast: $x \cdot v = x \cdot v$

Informal description

For any integer $x$ and vector $v : m \to \alpha$, the matrix-vector product of the scalar $x$ (viewed as a diagonal matrix) with $v$ is equal to the scalar multiplication of $x$ (in $\alpha$) with $v$, i.e., $$ x \cdot v = x \cdot v. $$

Matrix.vecMul_intCast theorem

(x : ℤ) (v : m → α) : v ᵥ* x = MulOpposite.op (x : α) • v

Full source

@[simp]
theorem vecMul_intCast (x : ℤ) (v : m → α) : v ᵥ* x = MulOpposite.op (x : α) • v :=
  vecMul_diagonal_const _ _

Vector-Scalar Multiplication via Multiplicative Opposite: $v \cdot x = x^{\text{op}} \cdot v$

Informal description

For any integer $x$ and vector $v : m \to \alpha$, the vector-matrix product of $v$ with the scalar $x$ (viewed as a diagonal matrix) equals the scalar multiplication of the multiplicative opposite of $x$ (in $\alpha$) with the vector $v$. That is, $$ v \cdot x = x^{\text{op}} \cdot v. $$

Matrix.transpose_mul theorem

[AddCommMonoid α] [CommMagma α] [Fintype n] (M : Matrix m n α) (N : Matrix n l α) : (M * N)ᵀ = Nᵀ * Mᵀ

Full source

@[simp]
theorem transpose_mul [AddCommMonoid α] [CommMagma α] [Fintype n] (M : Matrix m n α)
    (N : Matrix n l α) : (M * N)ᵀ = Nᵀ * Mᵀ := by
  ext
  apply dotProduct_comm

Transpose of Matrix Product: $(M * N)^\top = N^\top * M^\top$

Informal description

Let $\alpha$ be an additive commutative monoid with a commutative multiplication operation, and let $n$ be a finite type. For any matrices $M \in \text{Matrix}\, m\, n\, \alpha$ and $N \in \text{Matrix}\, n\, l\, \alpha$, the transpose of their product satisfies $(M * N)^\top = N^\top * M^\top$, where $*$ denotes matrix multiplication and $^\top$ denotes the transpose operation.

Matrix.submatrix_mul theorem

 [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p q : Type*} (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₃

Full source

theorem submatrix_mul [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p q : Type*}
    (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₃ :=
  ext fun _ _ => (he₂.sum_comp _).symm

Submatrix of Matrix Product under Bijective Reindexing

Informal description

Let $m$, $n$, $o$, $p$, $q$, $l$ be types, and let $\alpha$ be a type equipped with a multiplication operation and an additive commutative monoid structure. Suppose $n$ and $o$ are finite types. Given matrices $M \in \mathrm{Matrix}\, m\, n\, \alpha$ and $N \in \mathrm{Matrix}\, n\, p\, \alpha$, and reindexing functions $e_1 : l \to m$, $e_2 : o \to n$, $e_3 : q \to p$ such that $e_2$ is bijective, then the submatrix of the product $M * N$ with row reindexing $e_1$ and column reindexing $e_3$ is equal to the product of the submatrices of $M$ and $N$ with the corresponding reindexings. That is, $$(M * N).\mathrm{submatrix}\, e_1\, e_3 = M.\mathrm{submatrix}\, e_1\, e_2 * N.\mathrm{submatrix}\, e_2\, e_3.$$

Matrix.submatrix_mul_equiv theorem

 [Fintype n] [Fintype o] [AddCommMonoid α] [Mul α] {p q : Type*} (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₃

Full source

@[simp]
theorem submatrix_mul_equiv [Fintype n] [Fintype o] [AddCommMonoid α] [Mul α] {p q : Type*}
    (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₃ :=
  (submatrix_mul M N e₁ e₂ e₃ e₂.bijective).symm

Submatrix Multiplication via Equivalence: $M_{e_1,e_2} * N_{e_2,e_3} = (M * N)_{e_1,e_3}$

Informal description

Let $m$, $n$, $o$, $p$, $q$, $l$ be types, and let $\alpha$ be a type equipped with a multiplication operation and an additive commutative monoid structure. Suppose $n$ and $o$ are finite types. Given matrices $M \in \mathrm{Matrix}\, m\, n\, \alpha$ and $N \in \mathrm{Matrix}\, n\, p\, \alpha$, and reindexing functions $e_1 : l \to m$, $e_2 : o \simeq n$ (a bijective equivalence), and $e_3 : q \to p$, then the product of the submatrices $M.\mathrm{submatrix}\, e_1\, e_2$ and $N.\mathrm{submatrix}\, e_2\, e_3$ is equal to the submatrix of the product $M * N$ with row reindexing $e_1$ and column reindexing $e_3$. That is, $$M.\mathrm{submatrix}\, e_1\, e_2 * N.\mathrm{submatrix}\, e_2\, e_3 = (M * N).\mathrm{submatrix}\, e_1\, e_3.$$

Matrix.submatrix_mulVec_equiv theorem

 [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : o → α) (e₁ : l → m) (e₂ : o ≃ n) :
  M.submatrix e₁ e₂ *ᵥ v = (M *ᵥ (v ∘ e₂.symm)) ∘ e₁

Full source

theorem submatrix_mulVec_equiv [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α]
    (M : Matrix m n α) (v : o → α) (e₁ : l → m) (e₂ : o ≃ n) :
    M.submatrix e₁ e₂ *ᵥ v = (M *ᵥ (v ∘ e₂.symm)) ∘ e₁ :=
  funext fun _ => Eq.symm (dotProduct_comp_equiv_symm _ _ _)

Matrix-Vector Multiplication for Submatrix under Equivalence Reindexing

Informal description

Let $m$, $n$, $o$, $l$ be types, and let $\alpha$ be a non-unital non-associative semiring. Suppose $n$ and $o$ are finite types. Given a matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$, a vector $v : o \to \alpha$, a row reindexing function $e_1 : l \to m$, and an equivalence $e_2 : o \simeq n$, then the matrix-vector product of the submatrix $M.\mathrm{submatrix}\, e_1\, e_2$ with $v$ equals the composition of $e_1$ with the matrix-vector product of $M$ and $v \circ e_2^{-1}$. That is, $$(M.\mathrm{submatrix}\, e_1\, e_2) \cdot v = (M \cdot (v \circ e_2^{-1})) \circ e_1.$$

Matrix.submatrix_id_mul_left theorem

 [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type*} (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

Full source

@[simp]
theorem submatrix_id_mul_left [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type*}
    (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 := by
  ext; simp [mul_apply, ← e₂.bijective.sum_comp]

Left Submatrix Multiplication Identity with Equivalence

Informal description

Let $m$, $n$, $o$, and $p$ be finite types, and let $\alpha$ be a type equipped with multiplication and an additive commutative monoid structure. Given matrices $M \in \mathrm{Matrix}\, m\, n\, \alpha$ and $N \in \mathrm{Matrix}\, o\, p\, \alpha$, a function $e_1 : l \to m$, and an equivalence $e_2 : n \simeq o$, the product of the submatrix $M.\mathrm{submatrix}\, e_1\, \mathrm{id}$ with the submatrix $N.\mathrm{submatrix}\, e_2\, \mathrm{id}$ is equal to the product of the submatrix $M.\mathrm{submatrix}\, e_1\, e_2^{-1}$ with $N$. That is, \[ M.\mathrm{submatrix}\, e_1\, \mathrm{id} \cdot N.\mathrm{submatrix}\, e_2\, \mathrm{id} = M.\mathrm{submatrix}\, e_1\, e_2^{-1} \cdot N. \]

Matrix.submatrix_id_mul_right theorem

 [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type*} (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₁

Full source

@[simp]
theorem submatrix_id_mul_right [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type*}
    (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₁ := by
  ext; simp [mul_apply, ← e₂.bijective.sum_comp]

Right Submatrix Multiplication Identity with Equivalence

Informal description

Let $m$, $n$, $o$, $p$ be finite types, and let $\alpha$ be a type equipped with multiplication and an additive commutative monoid structure. For any matrices $M \in \mathrm{Matrix}\, m\, n\, \alpha$ and $N \in \mathrm{Matrix}\, o\, p\, \alpha$, and any functions $e_1 : l \to p$ and $e_2 : o \simeq n$, the following equality holds: \[ M.\mathrm{submatrix}\, \mathrm{id}\, e_2 * N.\mathrm{submatrix}\, \mathrm{id}\, e_1 = M * N.\mathrm{submatrix}\, e_2^{-1}\, e_1. \] Here, $\mathrm{id}$ denotes the identity function, and $e_2^{-1}$ is the inverse of the equivalence $e_2$.

Matrix.submatrix_vecMul_equiv theorem

 [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : l → α) (e₁ : l ≃ m) (e₂ : o → n) :
  v ᵥ* M.submatrix e₁ e₂ = ((v ∘ e₁.symm) ᵥ* M) ∘ e₂

Full source

theorem submatrix_vecMul_equiv [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α]
    (M : Matrix m n α) (v : l → α) (e₁ : l ≃ m) (e₂ : o → n) :
    v ᵥ* M.submatrix e₁ e₂ = ((v ∘ e₁.symm) ᵥ* M) ∘ e₂ :=
  funext fun _ => Eq.symm (comp_equiv_symm_dotProduct _ _ _)

Equivariant Submatrix Vector-Matrix Multiplication

Informal description

Let $l$, $m$, and $n$ be finite types, and let $\alpha$ be a non-unital non-associative semiring. Given a matrix $M : \text{Matrix}\, m\, n\, \alpha$, a vector $v : l \to \alpha$, an equivalence $e_1 : l \simeq m$, and a function $e_2 : o \to n$, the vector-matrix product of $v$ with the submatrix $M.\text{submatrix}\, e_1\, e_2$ is equal to the composition of the vector-matrix product of $v \circ e_1^{-1}$ with $M$ and the function $e_2$. That is, \[ v \cdot (M.\text{submatrix}\, e_1\, e_2) = (v \circ e_1^{-1} \cdot M) \circ e_2. \]

Matrix.mul_submatrix_one theorem

 [Fintype n] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : n ≃ o) (e₂ : l → o) (M : Matrix m n α) :
  M * (1 : Matrix o o α).submatrix e₁ e₂ = submatrix M id (e₁.symm ∘ e₂)

Full source

theorem mul_submatrix_one [Fintype n] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : n ≃ o)
    (e₂ : l → o) (M : Matrix m n α) :
    M * (1 : Matrix o o α).submatrix e₁ e₂ = submatrix M id (e₁.symm ∘ e₂) := by
  cases nonempty_fintype o
  let A := M.submatrix id e₁.symm
  have : M = A.submatrix id e₁ := by
    simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
  rw [this, submatrix_mul_equiv]
  simp only [A, Matrix.mul_one, submatrix_submatrix, Function.comp_id, submatrix_id_id,
    Equiv.symm_comp_self]

Right Multiplication by Submatrix of Identity Matrix: $M \cdot I_{e_1,e_2} = M_{\mathrm{id}, e_1^{-1} \circ e_2}$

Informal description

Let $m$, $n$, $o$, and $l$ be types, where $n$ is finite and $o$ is finite. Let $\alpha$ be a non-associative semiring with decidable equality on $o$. Given an equivalence $e_1 : n \simeq o$, a function $e_2 : l \to o$, and a matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$, the product of $M$ with the submatrix of the identity matrix of size $o \times o$ (reindexed by $e_1$ for rows and $e_2$ for columns) equals the submatrix of $M$ obtained by keeping rows unchanged and composing column indices with $e_1^{-1} \circ e_2$. That is, $$ M * (I_o).\mathrm{submatrix}\, e_1\, e_2 = M.\mathrm{submatrix}\, \mathrm{id}\, (e_1^{-1} \circ e_2). $$

Matrix.one_submatrix_mul theorem

 [Fintype m] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : l → o) (e₂ : m ≃ o) (M : Matrix m n α) :
  ((1 : Matrix o o α).submatrix e₁ e₂) * M = submatrix M (e₂.symm ∘ e₁) id

Full source

theorem one_submatrix_mul [Fintype m] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : l → o)
    (e₂ : m ≃ o) (M : Matrix m n α) :
    ((1 : Matrix o o α).submatrix e₁ e₂) * M = submatrix M (e₂.symm ∘ e₁) id := by
  cases nonempty_fintype o
  let A := M.submatrix e₂.symm id
  have : M = A.submatrix e₂ id := by
    simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
  rw [this, submatrix_mul_equiv]
  simp only [A, Matrix.one_mul, submatrix_submatrix, Function.comp_id, submatrix_id_id,
    Equiv.symm_comp_self]

Left Multiplication by Submatrix of Identity Matrix: $(1_{o \times o})_{e_1,e_2} * M = M_{e_2^{-1} \circ e_1, \mathrm{id}}$

Informal description

Let $m$, $o$, $l$, and $n$ be types, with $m$ finite and $o$ finite. Let $\alpha$ be a non-associative semiring with decidable equality on $o$. Given a matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$, an indexing function $e_1 : l \to o$, and an equivalence $e_2 : m \simeq o$, the product of the submatrix $(1 : \mathrm{Matrix}\, o\, o\, \alpha).\mathrm{submatrix}\, e_1\, e_2$ with $M$ equals the submatrix of $M$ obtained by reindexing rows via $e_2^{-1} \circ e_1$ and leaving columns unchanged. That is, $$(1_{o \times o}).\mathrm{submatrix}\, e_1\, e_2 * M = M.\mathrm{submatrix}\, (e_2^{-1} \circ e_1)\, \mathrm{id}.$$

Matrix.submatrix_mul_transpose_submatrix theorem

 [Fintype m] [Fintype n] [AddCommMonoid α] [Mul α] (e : m ≃ n) (M : Matrix m n α) :
  M.submatrix id e * Mᵀ.submatrix e id = M * Mᵀ

Full source

theorem submatrix_mul_transpose_submatrix [Fintype m] [Fintype n] [AddCommMonoid α] [Mul α]
    (e : m ≃ n) (M : Matrix m n α) : M.submatrix id e * Mᵀ.submatrix e id = M * Mᵀ := by
  rw [submatrix_mul_equiv, submatrix_id_id]

Submatrix Product Identity: $M_{\mathrm{id},e} * (M^\top)_{e,\mathrm{id}} = M * M^\top$

Informal description

Let $m$ and $n$ be finite types, and let $\alpha$ be a type equipped with a multiplication operation and an additive commutative monoid structure. For any bijection $e : m \simeq n$ and any matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$, the product of the submatrix $M.\mathrm{submatrix}\, \mathrm{id}\, e$ (where rows are kept the same and columns are reindexed by $e$) with the submatrix $M^\top.\mathrm{submatrix}\, e\, \mathrm{id}$ (the transpose of $M$ with rows reindexed by $e$ and columns kept the same) equals the product $M * M^\top$. In other words, for any matrix $M$ and bijection $e$ between its row and column index types, we have: $$ M_{\mathrm{id},e} * (M^\top)_{e,\mathrm{id}} = M * M^\top $$

RingHom.map_matrix_mul theorem

(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

Full source

theorem map_matrix_mul (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 := by
  simp [Matrix.mul_apply, map_sum]

Ring Homomorphism Preserves Matrix Multiplication Entrywise

Informal description

Let $R$ and $S$ be rings, and let $f : R \to S$ be a ring homomorphism. For any matrices $M \in \mathrm{Mat}_{m \times n}(R)$ and $N \in \mathrm{Mat}_{n \times o}(R)$, and for any indices $i \in m$ and $j \in o$, the homomorphism $f$ applied to the $(i,j)$-th entry of the matrix product $M * N$ equals the $(i,j)$-th entry of the product of the entry-wise mapped matrices $f \circ M$ and $f \circ N$. In other words, $$ f\big((M * N)_{i,j}\big) = (f \circ M * f \circ N)_{i,j}. $$

RingHom.map_dotProduct theorem

[NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (v w : n → R) : f (v ⬝ᵥ w) = f ∘ v ⬝ᵥ f ∘ w

Full source

theorem map_dotProduct [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (v w : n → R) :
    f (v ⬝ᵥ w) = f ∘ vf ∘ v ⬝ᵥ f ∘ w := by
  simp only [dotProduct, map_sum f, f.map_mul, Function.comp]

Ring Homomorphism Preserves Dot Product

Informal description

Let $R$ and $S$ be non-associative semirings, and let $f : R \to S$ be a ring homomorphism. For any vectors $v, w : n \to R$, the image of their dot product under $f$ equals the dot product of their images under $f$, i.e., $$ f(v \cdot w) = (f \circ v) \cdot (f \circ w). $$

RingHom.map_vecMul theorem

 [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix n m R) (v : n → R) (i : m) :
  f ((v ᵥ* M) i) = ((f ∘ v) ᵥ* M.map f) i

Full source

theorem map_vecMul [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix n m R)
    (v : n → R) (i : m) : f ((v ᵥ* M) i) =  ((f ∘ v) ᵥ* M.map f) i := by
  simp only [Matrix.vecMul, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]

Ring Homomorphism Preserves Vector-Matrix Multiplication Componentwise

Informal description

Let $R$ and $S$ be non-associative semirings, and let $f : R \to S$ be a ring homomorphism. For any matrix $M \in \text{Matrix}\, n\, m\, R$ and vector $v : n \to R$, the image under $f$ of the $i$-th component of the vector-matrix product $v \cdot M$ equals the $i$-th component of the vector-matrix product $(f \circ v) \cdot (M.map\, f)$. In other words, $$ f\big((v \cdot M)_i\big) = \big((f \circ v) \cdot (M.map\, f)\big)_i. $$

RingHom.map_mulVec theorem

 [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix m n R) (v : n → R) (i : m) :
  f ((M *ᵥ v) i) = (M.map f *ᵥ (f ∘ v)) i

Full source

theorem map_mulVec [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix m n R)
    (v : n → R) (i : m) : f ((M *ᵥ v) i) = (M.map f *ᵥ (f ∘ v)) i := by
  simp only [Matrix.mulVec, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]

Ring Homomorphism Preserves Matrix-Vector Multiplication Entrywise

Informal description

Let $R$ and $S$ be non-associative semirings, and let $f : R \to S$ be a ring homomorphism. For any matrix $M$ of size $m \times n$ with entries in $R$, any vector $v$ of size $n$ with entries in $R$, and any index $i \in m$, the image under $f$ of the $i$-th entry of the matrix-vector product $M \cdot v$ equals the $i$-th entry of the matrix-vector product obtained by applying $f$ entry-wise to $M$ and component-wise to $v$, i.e., $$ f\big((M \cdot v)_i\big) = \big(f(M) \cdot f(v)\big)_i. $$

Mathlib.Data.Matrix.Mul

Main definitions

Notation

Implementation notes

TODO