doc-next-gen

Mathlib.Data.Matrix.Basis

Module docstring

{"# Matrices with a single non-zero element.

This file provides Matrix.stdBasisMatrix. The matrix Matrix.stdBasisMatrix i j c has c at position (i, j), and zeroes elsewhere. "}

Matrix.stdBasisMatrix definition
(i : m) (j : n) (a : α) : Matrix m n α
Full source 
/-- `stdBasisMatrix i j a` is the matrix with `a` in the `i`-th row, `j`-th column,
and zeroes elsewhere.
-/
def stdBasisMatrix (i : m) (j : n) (a : α) : Matrix m n α :=
  of <| fun i' j' => if i = i' ∧ j = j' then a else 0
Standard basis matrix with single non-zero entry
Informal description
The matrix $\text{stdBasisMatrix}\, i\, j\, a$ is the matrix with entry $a$ at position $(i, j)$ and zeros elsewhere. Formally, it is defined as the matrix where the entry at $(i', j')$ is $a$ if $i = i'$ and $j = j'$, and $0$ otherwise.
Matrix.stdBasisMatrix_eq_of_single_single theorem
(i : m) (j : n) (a : α) : stdBasisMatrix i j a = Matrix.of (Pi.single i (Pi.single j a))
Full source 
theorem stdBasisMatrix_eq_of_single_single (i : m) (j : n) (a : α) :
    stdBasisMatrix i j a = Matrix.of (Pi.single i (Pi.single j a)) := by
  ext a b
  unfold stdBasisMatrix
  by_cases hi : i = a <;> by_cases hj : j = b <;> simp [*]
Standard Basis Matrix as Single-Single Function Matrix
Informal description
For any row index $i \in m$, column index $j \in n$, and entry $a \in \alpha$, the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, a$ is equal to the matrix constructed from the function $\text{Pi.single}\, i\, (\text{Pi.single}\, j\, a)$, where $\text{Pi.single}$ denotes the function that is zero everywhere except at the specified index.
Matrix.of_symm_stdBasisMatrix theorem
(i : m) (j : n) (a : α) : of.symm (stdBasisMatrix i j a) = Pi.single i (Pi.single j a)
Full source 
@[simp]
theorem of_symm_stdBasisMatrix (i : m) (j : n) (a : α) :
    of.symm (stdBasisMatrix i j a) = Pi.single i (Pi.single j a) :=
  congr_arg of.symm <| stdBasisMatrix_eq_of_single_single i j a
Underlying Function Representation of Standard Basis Matrix: $\text{of}^{-1}(E_{ij}(a)) = \text{single}_i \circ \text{single}_j(a)$
Informal description
For any row index $i \in m$, column index $j \in n$, and entry $a \in \alpha$, the inverse of the matrix construction function applied to the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, a$ yields the function $\text{Pi.single}\, i\, (\text{Pi.single}\, j\, a)$, where $\text{Pi.single}$ denotes the function that is zero everywhere except at the specified index. In other words, the underlying function representation of the standard basis matrix with entry $a$ at position $(i,j)$ is the pointwise single function at $i$ composed with the pointwise single function at $j$ evaluated at $a$.
Matrix.smul_stdBasisMatrix theorem
[SMulZeroClass R α] (r : R) (i : m) (j : n) (a : α) : r • stdBasisMatrix i j a = stdBasisMatrix i j (r • a)
Full source 
@[simp]
theorem smul_stdBasisMatrix [SMulZeroClass R α] (r : R) (i : m) (j : n) (a : α) :
    r • stdBasisMatrix i j a = stdBasisMatrix i j (r • a) := by
  unfold stdBasisMatrix
  ext
  simp [smul_ite]
Scalar Multiplication of Standard Basis Matrix: $r \cdot E_{ij}(a) = E_{ij}(r \cdot a)$
Informal description
Let $R$ be a type with a scalar multiplication operation on a type $\alpha$ such that $0$ is absorbing (i.e., $r \cdot 0 = 0$ for all $r \in R$). For any scalar $r \in R$, indices $i \in m$, $j \in n$, and element $a \in \alpha$, the scalar multiple of the standard basis matrix satisfies: \[ r \cdot \text{stdBasisMatrix}\, i\, j\, a = \text{stdBasisMatrix}\, i\, j\, (r \cdot a). \] Here, $\text{stdBasisMatrix}\, i\, j\, a$ denotes the matrix with entry $a$ at position $(i,j)$ and zeros elsewhere.
Matrix.stdBasisMatrix_zero theorem
(i : m) (j : n) : stdBasisMatrix i j (0 : α) = 0
Full source 
@[simp]
theorem stdBasisMatrix_zero (i : m) (j : n) : stdBasisMatrix i j (0 : α) = 0 := by
  unfold stdBasisMatrix
  ext
  simp
Standard Basis Matrix with Zero Entry is Zero Matrix
Informal description
For any row index $i \in m$ and column index $j \in n$, the standard basis matrix with entry $0$ at position $(i,j)$ is equal to the zero matrix. That is, $\text{stdBasisMatrix}\, i\, j\, 0 = 0$.
Matrix.transpose_stdBasisMatrix theorem
(i : m) (j : n) (a : α) : (stdBasisMatrix i j a)ᵀ = stdBasisMatrix j i a
Full source 
@[simp]
lemma transpose_stdBasisMatrix (i : m) (j : n) (a : α) :
    (stdBasisMatrix i j a)ᵀ = stdBasisMatrix j i a := by
  aesop (add unsafe unfold stdBasisMatrix)
Transpose of Standard Basis Matrix Swaps Indices
Informal description
For any row index $i \in m$, column index $j \in n$, and entry $a \in \alpha$, the transpose of the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, a$ is equal to the standard basis matrix $\text{stdBasisMatrix}\, j\, i\, a$. In other words, $(\text{stdBasisMatrix}\, i\, j\, a)^\top = \text{stdBasisMatrix}\, j\, i\, a$.
Matrix.map_stdBasisMatrix theorem
(i : m) (j : n) (a : α) {β : Type*} [Zero β] {F : Type*} [FunLike F α β] [ZeroHomClass F α β] (f : F) : (stdBasisMatrix i j a).map f = stdBasisMatrix i j (f a)
Full source 
@[simp]
lemma map_stdBasisMatrix (i : m) (j : n) (a : α) {β : Type*} [Zero β]
    {F : Type*} [FunLike F α β] [ZeroHomClass F α β] (f : F) :
    (stdBasisMatrix i j a).map f = stdBasisMatrix i j (f a) := by
  aesop (add unsafe unfold stdBasisMatrix)
Mapping Preserves Standard Basis Matrix Structure
Informal description
Let $m$ and $n$ be types indexing the rows and columns of matrices, respectively, and let $\alpha$ and $\beta$ be types with zero elements. Given a zero-preserving function $f : \alpha \to \beta$ (i.e., $f(0) = 0$), for any indices $i \in m$, $j \in n$, and element $a \in \alpha$, the entrywise application of $f$ to the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, a$ yields the standard basis matrix with $f(a)$ at position $(i,j)$ and zeros elsewhere. That is, $$ \text{map}\, (\text{stdBasisMatrix}\, i\, j\, a)\, f = \text{stdBasisMatrix}\, i\, j\, (f a). $$
Matrix.stdBasisMatrix_add theorem
[AddZeroClass α] (i : m) (j : n) (a b : α) : stdBasisMatrix i j (a + b) = stdBasisMatrix i j a + stdBasisMatrix i j b
Full source 
theorem stdBasisMatrix_add [AddZeroClass α] (i : m) (j : n) (a b : α) :
    stdBasisMatrix i j (a + b) = stdBasisMatrix i j a + stdBasisMatrix i j b := by
  ext
  simp only [stdBasisMatrix, of_apply]
  split_ifs with h <;> simp [h]
Additivity of Standard Basis Matrix Construction: $\text{stdBasisMatrix}\, i\, j\, (a + b) = \text{stdBasisMatrix}\, i\, j\, a + \text{stdBasisMatrix}\, i\, j\, b$
Informal description
Let $\alpha$ be a type with an addition operation that has a zero element (i.e., an `AddZeroClass`). For any indices $i \in m$ and $j \in n$, and any elements $a, b \in \alpha$, the standard basis matrix with entry $a + b$ at position $(i,j)$ is equal to the sum of the standard basis matrices with entries $a$ and $b$ at position $(i,j)$. That is, \[ \text{stdBasisMatrix}\, i\, j\, (a + b) = \text{stdBasisMatrix}\, i\, j\, a + \text{stdBasisMatrix}\, i\, j\, b. \]
Matrix.mulVec_stdBasisMatrix theorem
[NonUnitalNonAssocSemiring α] [Fintype m] (i : n) (j : m) (c : α) (x : m → α) : mulVec (stdBasisMatrix i j c) x = Function.update (0 : n → α) i (c * x j)
Full source 
theorem mulVec_stdBasisMatrix [NonUnitalNonAssocSemiring α] [Fintype m]
    (i : n) (j : m) (c : α) (x : m → α) :
    mulVec (stdBasisMatrix i j c) x = Function.update (0 : n → α) i (c * x j) := by
  ext i'
  simp [stdBasisMatrix, mulVec, dotProduct]
  rcases eq_or_ne i i' with rfl|h
  · simp
  simp [h, h.symm]
Matrix-vector product of a standard basis matrix
Informal description
Let $\alpha$ be a non-unital non-associative semiring, and let $m$ be a finite type. For any indices $i \in n$ and $j \in m$, any scalar $c \in \alpha$, and any vector $x : m \to \alpha$, the matrix-vector product of the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, c$ with $x$ is equal to the function that is zero everywhere except at index $i$, where it takes the value $c \cdot x_j$. Formally, this can be written as: \[ \text{stdBasisMatrix}\, i\, j\, c \cdot x = \text{update}\, (\lambda \_, 0)\, i\, (c \cdot x_j) \] where $\text{update}$ modifies the zero function to have value $c \cdot x_j$ at $i$.
Matrix.matrix_eq_sum_stdBasisMatrix theorem
[AddCommMonoid α] [Fintype m] [Fintype n] (x : Matrix m n α) : x = ∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)
Full source 
theorem matrix_eq_sum_stdBasisMatrix [AddCommMonoid α] [Fintype m] [Fintype n] (x : Matrix m n α) :
    x = ∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j) := by
  ext i j
  rw [← Fintype.sum_prod_type']
  simp [stdBasisMatrix, Matrix.sum_apply, Matrix.of_apply, ← Prod.mk_inj]
Matrix Decomposition into Standard Basis Matrices: $x = \sum_{i,j} \mathrm{stdBasisMatrix}\, i\, j\, x_{ij}$
Informal description
Let $\alpha$ be an additive commutative monoid, and let $m$ and $n$ be finite types. For any matrix $x \in \mathrm{Matrix}\, m\, n\, \alpha$, the matrix $x$ can be expressed as the sum of standard basis matrices: \[ x = \sum_{i \in m} \sum_{j \in n} \mathrm{stdBasisMatrix}\, i\, j\, (x_{ij}), \] where $\mathrm{stdBasisMatrix}\, i\, j\, (x_{ij})$ is the matrix with entry $x_{ij}$ at position $(i,j)$ and zeros elsewhere.
Matrix.stdBasisMatrix_eq_single_vecMulVec_single theorem
[MulZeroOneClass α] (i : m) (j : n) : stdBasisMatrix i j (1 : α) = vecMulVec (Pi.single i 1) (Pi.single j 1)
Full source 
theorem stdBasisMatrix_eq_single_vecMulVec_single [MulZeroOneClass α] (i : m) (j : n) :
    stdBasisMatrix i j (1 : α) = vecMulVec (Pi.single i 1) (Pi.single j 1) := by
  ext i' j'
  simp [-mul_ite, stdBasisMatrix, vecMulVec, ite_and, Pi.single_apply, eq_comm]
Standard Basis Matrix as Outer Product of Standard Basis Vectors
Informal description
Let $\alpha$ be a type with a multiplicative zero-one class structure. For any indices $i \in m$ and $j \in n$, the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, 1$ is equal to the outer product of the standard basis vectors $\text{Pi.single}\, i\, 1$ and $\text{Pi.single}\, j\, 1$. Formally, this can be written as: \[ \text{stdBasisMatrix}\, i\, j\, 1 = \text{vecMulVec}\, (\text{Pi.single}\, i\, 1)\, (\text{Pi.single}\, j\, 1) \] where $\text{vecMulVec}$ denotes the outer product operation.
Matrix.induction_on' theorem
[AddCommMonoid α] [Finite m] [Finite n] {P : Matrix m n α → Prop} (M : Matrix m n α) (h_zero : P 0) (h_add : ∀ p q, P p → P q → P (p + q)) (h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)) : P M
Full source 
@[elab_as_elim]
protected theorem induction_on'
    [AddCommMonoid α] [Finite m] [Finite n] {P : Matrix m n α → Prop} (M : Matrix m n α)
    (h_zero : P 0) (h_add : ∀ p q, P p → P q → P (p + q))
    (h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)) : P M := by
  cases nonempty_fintype m; cases nonempty_fintype n
  rw [matrix_eq_sum_stdBasisMatrix M, ← Finset.sum_product']
  apply Finset.sum_induction _ _ h_add h_zero
  · intros
    apply h_std_basis
Induction Principle for Matrices over Finite Index Types
Informal description
Let $\alpha$ be an additive commutative monoid, and let $m$ and $n$ be finite types. For any matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$ and any predicate $P$ on matrices, if: 1. $P$ holds for the zero matrix, 2. $P$ is preserved under matrix addition (i.e., for any matrices $p$ and $q$, if $P(p)$ and $P(q)$ hold, then $P(p + q)$ holds), and 3. $P$ holds for all standard basis matrices $\mathrm{stdBasisMatrix}\, i\, j\, x$ for any $i \in m$, $j \in n$, and $x \in \alpha$, then $P(M)$ holds.
Matrix.induction_on theorem
[AddCommMonoid α] [Finite m] [Finite n] [Nonempty m] [Nonempty n] {P : Matrix m n α → Prop} (M : Matrix m n α) (h_add : ∀ p q, P p → P q → P (p + q)) (h_std_basis : ∀ i j x, P (stdBasisMatrix i j x)) : P M
Full source 
@[elab_as_elim]
protected theorem induction_on
    [AddCommMonoid α] [Finite m] [Finite n] [Nonempty m] [Nonempty n]
    {P : Matrix m n α → Prop} (M : Matrix m n α) (h_add : ∀ p q, P p → P q → P (p + q))
    (h_std_basis : ∀ i j x, P (stdBasisMatrix i j x)) : P M :=
  Matrix.induction_on' M
    (by
      inhabit m
      inhabit n
      simpa using h_std_basis default default 0)
    h_add h_std_basis
Matrix Induction Principle for Finite Nonempty Index Types
Informal description
Let $\alpha$ be an additive commutative monoid, and let $m$ and $n$ be finite nonempty types. For any matrix $M \in \mathrm{Matrix}\, m\, n\, \alpha$ and any predicate $P$ on matrices, if: 1. $P$ is preserved under matrix addition (i.e., for any matrices $p$ and $q$, if $P(p)$ and $P(q)$ hold, then $P(p + q)$ holds), and 2. $P$ holds for all standard basis matrices $\mathrm{stdBasisMatrix}\, i\, j\, x$ for any $i \in m$, $j \in n$, and $x \in \alpha$, then $P(M)$ holds.
Matrix.stdBasisMatrixAddMonoidHom definition
[AddCommMonoid α] (i : m) (j : n) : α →+ Matrix m n α
Full source 
/-- `Matrix.stdBasisMatrix` as a bundled additive map. -/
@[simps]
def stdBasisMatrixAddMonoidHom [AddCommMonoid α] (i : m) (j : n) : α →+ Matrix m n α where
  toFun := stdBasisMatrix i j
  map_zero' := stdBasisMatrix_zero _ _
  map_add' _ _ := stdBasisMatrix_add _ _ _ _
Additive monoid homomorphism version of standard basis matrix construction
Informal description
For any additive commutative monoid $\alpha$, the function $\text{stdBasisMatrixAddMonoidHom}\, i\, j$ maps an element $a \in \alpha$ to the matrix with $a$ at position $(i,j)$ and zeros elsewhere, and this mapping is an additive monoid homomorphism. That is, it satisfies: 1. $\text{stdBasisMatrixAddMonoidHom}\, i\, j\, 0 = 0$ (the zero matrix) 2. $\text{stdBasisMatrixAddMonoidHom}\, i\, j\, (a + b) = \text{stdBasisMatrixAddMonoidHom}\, i\, j\, a + \text{stdBasisMatrixAddMonoidHom}\, i\, j\, b$ for all $a, b \in \alpha$
Matrix.stdBasisMatrixLinearMap definition
[Semiring R] [AddCommMonoid α] [Module R α] (i : m) (j : n) : α →ₗ[R] Matrix m n α
Full source 
/-- `Matrix.stdBasisMatrix` as a bundled linear map. -/
@[simps!]
def stdBasisMatrixLinearMap [Semiring R] [AddCommMonoid α] [Module R α] (i : m) (j : n) :
    α →ₗ[R] Matrix m n α where
  __ := stdBasisMatrixAddMonoidHom i j
  map_smul' _ _:= smul_stdBasisMatrix _ _ _ _ |>.symm
Linear map version of standard basis matrix construction
Informal description
For a semiring $R$ and an additive commutative monoid $\alpha$ equipped with a module structure over $R$, the function $\text{stdBasisMatrixLinearMap}\, R\, i\, j$ maps an element $a \in \alpha$ to the matrix with $a$ at position $(i,j)$ and zeros elsewhere, and this mapping is a linear map over $R$. That is, it satisfies: 1. $\text{stdBasisMatrixLinearMap}\, R\, i\, j\, (a + b) = \text{stdBasisMatrixLinearMap}\, R\, i\, j\, a + \text{stdBasisMatrixLinearMap}\, R\, i\, j\, b$ for all $a, b \in \alpha$ 2. $\text{stdBasisMatrixLinearMap}\, R\, i\, j\, (r \cdot a) = r \cdot \text{stdBasisMatrixLinearMap}\, R\, i\, j\, a$ for all $r \in R$ and $a \in \alpha$
Matrix.ext_addMonoidHom theorem
[Finite m] [Finite n] [AddCommMonoid α] [AddCommMonoid β] ⦃f g : Matrix m n α →+ β⦄ (h : ∀ i j, f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)) : f = g
Full source 
/-- Additive maps from finite matrices are equal if they agree on the standard basis.

See note [partially-applied ext lemmas]. -/
@[local ext]
theorem ext_addMonoidHom
    [Finite m] [Finite n] [AddCommMonoid α] [AddCommMonoid β] ⦃f g : MatrixMatrix m n α →+ β⦄
    (h : ∀ i j, f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)) :
    f = g := by
  cases nonempty_fintype m
  cases nonempty_fintype n
  ext x
  rw [matrix_eq_sum_stdBasisMatrix x]
  simp_rw [map_sum]
  congr! 2
  exact DFunLike.congr_fun (h _ _) _
Extensionality of Additive Monoid Homomorphisms on Matrices via Standard Basis
Informal description
Let $m$ and $n$ be finite types, and let $\alpha$ and $\beta$ be additive commutative monoids. For any two additive monoid homomorphisms $f, g \colon \mathrm{Matrix}\, m\, n\, \alpha \to \beta$, if for all indices $i \in m$ and $j \in n$ the compositions $f \circ \mathrm{stdBasisMatrixAddMonoidHom}\, i\, j$ and $g \circ \mathrm{stdBasisMatrixAddMonoidHom}\, i\, j$ are equal, then $f = g$.
Matrix.ext_linearMap theorem
[Finite m] [Finite n] [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] ⦃f g : Matrix m n α →ₗ[R] β⦄ (h : ∀ i j, f ∘ₗ stdBasisMatrixLinearMap R i j = g ∘ₗ stdBasisMatrixLinearMap R i j) : f = g
Full source 
/-- Linear maps from finite matrices are equal if they agree on the standard basis.

See note [partially-applied ext lemmas]. -/
@[local ext]
theorem ext_linearMap
    [Finite m] [Finite n] [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β]
    ⦃f g : MatrixMatrix m n α →ₗ[R] β⦄
    (h : ∀ i j, f ∘ₗ stdBasisMatrixLinearMap R i j = g ∘ₗ stdBasisMatrixLinearMap R i j) :
    f = g :=
  LinearMap.toAddMonoidHom_injective <| ext_addMonoidHom fun i j =>
    congrArg LinearMap.toAddMonoidHom <| h i j
Extensionality of Linear Maps on Matrices via Standard Basis
Informal description
Let $m$ and $n$ be finite types, let $R$ be a semiring, and let $\alpha$ and $\beta$ be additive commutative monoids equipped with $R$-module structures. For any two $R$-linear maps $f, g \colon \mathrm{Matrix}\, m\, n\, \alpha \to \beta$, if for all indices $i \in m$ and $j \in n$ the compositions $f \circ \mathrm{stdBasisMatrixLinearMap}\, R\, i\, j$ and $g \circ \mathrm{stdBasisMatrixLinearMap}\, R\, i\, j$ are equal, then $f = g$.
Matrix.StdBasisMatrix.apply_same theorem
: stdBasisMatrix i j c i j = c
Full source 
@[simp]
theorem apply_same : stdBasisMatrix i j c i j = c :=
  if_pos (And.intro rfl rfl)
Diagonal Entry of Standard Basis Matrix
Informal description
For any indices $i$, $j$ and any element $c$, the $(i,j)$-th entry of the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, c$ is equal to $c$.
Matrix.StdBasisMatrix.apply_of_ne theorem
(h : ¬(i = i' ∧ j = j')) : stdBasisMatrix i j c i' j' = 0
Full source 
@[simp]
theorem apply_of_ne (h : ¬(i = i' ∧ j = j')) : stdBasisMatrix i j c i' j' = 0 := by
  simp only [stdBasisMatrix, and_imp, ite_eq_right_iff, of_apply]
  tauto
Zero Entries in Standard Basis Matrix Outside $(i, j)$ Position
Informal description
For any indices $i, i'$ and $j, j'$, if it is not the case that both $i = i'$ and $j = j'$, then the entry at position $(i', j')$ in the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, c$ is zero, i.e., $(\text{stdBasisMatrix}\, i\, j\, c)_{i'j'} = 0$.
Matrix.StdBasisMatrix.apply_of_row_ne theorem
{i i' : m} (hi : i ≠ i') (j j' : n) (a : α) : stdBasisMatrix i j a i' j' = 0
Full source 
@[simp]
theorem apply_of_row_ne {i i' : m} (hi : i ≠ i') (j j' : n) (a : α) :
    stdBasisMatrix i j a i' j' = 0 := by simp [hi]
Zero Entries in Standard Basis Matrix for Different Rows
Informal description
For any indices $i \neq i'$ in the row indices and any indices $j, j'$ in the column indices, the entry at position $(i', j')$ in the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, a$ is zero, i.e., $(\text{stdBasisMatrix}\, i\, j\, a)_{i'j'} = 0$.
Matrix.StdBasisMatrix.apply_of_col_ne theorem
(i i' : m) {j j' : n} (hj : j ≠ j') (a : α) : stdBasisMatrix i j a i' j' = 0
Full source 
@[simp]
theorem apply_of_col_ne (i i' : m) {j j' : n} (hj : j ≠ j') (a : α) :
    stdBasisMatrix i j a i' j' = 0 := by simp [hj]
Zero Entries in Standard Basis Matrix for Non-Matching Column Indices
Informal description
For any indices $i, i'$ in $m$ and $j, j'$ in $n$, if $j \neq j'$, then the entry at position $(i', j')$ in the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, a$ is zero, i.e., $(\text{stdBasisMatrix}\, i\, j\, a)_{i'j'} = 0$.
Matrix.StdBasisMatrix.diag_zero theorem
(h : j ≠ i) : diag (stdBasisMatrix i j c) = 0
Full source 
@[simp]
theorem diag_zero (h : j ≠ i) : diag (stdBasisMatrix i j c) = 0 :=
  funext fun _ => if_neg fun ⟨e₁, e₂⟩ => h (e₂.trans e₁.symm)
Diagonal of Standard Basis Matrix is Zero for Off-Diagonal Entries
Informal description
For any indices $i$ and $j$ with $j \neq i$, the diagonal of the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, c$ is the zero function, i.e., $\text{diag}(\text{stdBasisMatrix}\, i\, j\, c) = 0$.
Matrix.StdBasisMatrix.diag_same theorem
: diag (stdBasisMatrix i i c) = Pi.single i c
Full source 
@[simp]
theorem diag_same : diag (stdBasisMatrix i i c) = Pi.single i c := by
  ext j
  by_cases hij : i = j <;> (try rw [hij]) <;> simp [hij]
Diagonal of Standard Basis Matrix at $(i,i)$ Equals Point Mass at $i$
Informal description
For any index $i$ and element $c$, the diagonal of the standard basis matrix $\text{stdBasisMatrix}\, i\, i\, c$ is equal to the function that is $c$ at index $i$ and zero elsewhere, i.e., $\text{diag}(\text{stdBasisMatrix}\, i\, i\, c) = \text{Pi.single}\, i\, c$.
Matrix.StdBasisMatrix.mul_left_apply_same theorem
(i : l) (j : m) (b : n) (M : Matrix m n α) : (stdBasisMatrix i j c * M) i b = c * M j b
Full source 
@[simp]
theorem mul_left_apply_same (i : l) (j : m) (b : n) (M : Matrix m n α) :
    (stdBasisMatrix i j c * M) i b = c * M j b := by simp [mul_apply, stdBasisMatrix]
Matrix multiplication with standard basis matrix preserves $(i,b)$-entry as scaled $(j,b)$-entry
Informal description
Let $i \in l$, $j \in m$, $b \in n$, and $M$ be an $m \times n$ matrix. Then the $(i, b)$-entry of the product of the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, c$ with $M$ is equal to $c$ multiplied by the $(j, b)$-entry of $M$, i.e., $$(\text{stdBasisMatrix}\, i\, j\, c \cdot M)_{i,b} = c \cdot M_{j,b}.$$
Matrix.StdBasisMatrix.mul_right_apply_same theorem
(i : m) (j : n) (a : l) (M : Matrix l m α) : (M * stdBasisMatrix i j c) a j = M a i * c
Full source 
@[simp]
theorem mul_right_apply_same (i : m) (j : n) (a : l) (M : Matrix l m α) :
    (M * stdBasisMatrix i j c) a j = M a i * c := by simp [mul_apply, stdBasisMatrix, mul_comm]
Matrix Multiplication with Standard Basis Matrix Preserves Entry at $(a, j)$
Informal description
For any matrix $M$ of size $l \times m$ with entries in type $\alpha$, and for any indices $i \in m$, $j \in n$, and $a \in l$, the $(a, j)$-th entry of the product $M \cdot \text{stdBasisMatrix}(i, j, c)$ equals $M_{a,i} \cdot c$, where $\text{stdBasisMatrix}(i, j, c)$ is the matrix with entry $c$ at position $(i, j)$ and zeros elsewhere.
Matrix.StdBasisMatrix.mul_left_apply_of_ne theorem
(i : l) (j : m) (a : l) (b : n) (h : a ≠ i) (M : Matrix m n α) : (stdBasisMatrix i j c * M) a b = 0
Full source 
@[simp]
theorem mul_left_apply_of_ne (i : l) (j : m) (a : l) (b : n) (h : a ≠ i) (M : Matrix m n α) :
    (stdBasisMatrix i j c * M) a b = 0 := by simp [mul_apply, h.symm]
Zero Entries in Product of Standard Basis Matrix and Arbitrary Matrix Outside Row $i$
Informal description
For any indices $i \in l$, $j \in m$, $a \in l$, $b \in n$ with $a \neq i$, and any $m \times n$ matrix $M$, the $(a, b)$-entry of the product $\text{stdBasisMatrix}(i, j, c) \cdot M$ is zero, i.e., $$(\text{stdBasisMatrix}(i, j, c) \cdot M)_{a,b} = 0.$$
Matrix.StdBasisMatrix.mul_right_apply_of_ne theorem
(i : m) (j : n) (a : l) (b : n) (hbj : b ≠ j) (M : Matrix l m α) : (M * stdBasisMatrix i j c) a b = 0
Full source 
@[simp]
theorem mul_right_apply_of_ne (i : m) (j : n) (a : l) (b : n) (hbj : b ≠ j) (M : Matrix l m α) :
    (M * stdBasisMatrix i j c) a b = 0 := by simp [mul_apply, hbj.symm]
Vanishing of Matrix Product Entries Outside Column $j$
Informal description
Let $M$ be an $l \times m$ matrix over a type $\alpha$, and let $\text{stdBasisMatrix}\, i\, j\, c$ be the $m \times n$ matrix with entry $c$ at position $(i,j)$ and zeros elsewhere. For any row index $a \in l$ and column index $b \in n$ with $b \neq j$, the $(a,b)$-th entry of the product $M \cdot \text{stdBasisMatrix}\, i\, j\, c$ is zero, i.e., $(M \cdot \text{stdBasisMatrix}\, i\, j\, c)_{a,b} = 0$.
Matrix.StdBasisMatrix.mul_same theorem
(i : l) (j : m) (k : n) (d : α) : stdBasisMatrix i j c * stdBasisMatrix j k d = stdBasisMatrix i k (c * d)
Full source 
@[simp]
theorem mul_same (i : l) (j : m) (k : n) (d : α) :
    stdBasisMatrix i j c * stdBasisMatrix j k d = stdBasisMatrix i k (c * d) := by
  ext a b
  simp only [mul_apply, stdBasisMatrix, boole_mul]
  by_cases h₁ : i = a <;> by_cases h₂ : k = b <;> simp [h₁, h₂]
Product of Standard Basis Matrices with Matching Middle Index
Informal description
For any indices $i \in l$, $j \in m$, $k \in n$ and any elements $c, d \in \alpha$, the product of the standard basis matrices $\text{stdBasisMatrix}\, i\, j\, c$ and $\text{stdBasisMatrix}\, j\, k\, d$ is equal to the standard basis matrix $\text{stdBasisMatrix}\, i\, k\, (c \cdot d)$. In other words, the product of two standard basis matrices with matching middle index $j$ is another standard basis matrix with the product of their entries at the corresponding position.
Matrix.StdBasisMatrix.stdBasisMatrix_mul_mul_stdBasisMatrix theorem
[Fintype n] (i : l) (i' : m) (j' : n) (j : o) (a : α) (x : Matrix m n α) (b : α) : stdBasisMatrix i i' a * x * stdBasisMatrix j' j b = stdBasisMatrix i j (a * x i' j' * b)
Full source 
@[simp]
theorem stdBasisMatrix_mul_mul_stdBasisMatrix [Fintype n]
    (i : l) (i' : m) (j' : n) (j : o) (a : α) (x : Matrix m n α) (b : α) :
    stdBasisMatrix i i' a * x * stdBasisMatrix j' j b = stdBasisMatrix i j (a * x i' j' * b) := by
  ext i'' j''
  simp only [mul_apply, stdBasisMatrix, boole_mul]
  by_cases h₁ : i = i'' <;> by_cases h₂ : j = j'' <;> simp [h₁, h₂]
Product of Standard Basis Matrices via Middle Matrix Entry
Informal description
Let $m$, $n$, $l$, and $o$ be finite types, and let $\alpha$ be a type with multiplication. For any indices $i \in l$, $i' \in m$, $j' \in n$, $j \in o$, any scalars $a, b \in \alpha$, and any matrix $x \in \text{Matrix}\, m\, n\, \alpha$, the product of the standard basis matrices satisfies: \[ \text{stdBasisMatrix}\, i\, i'\, a \cdot x \cdot \text{stdBasisMatrix}\, j'\, j\, b = \text{stdBasisMatrix}\, i\, j\, (a \cdot x_{i'j'} \cdot b). \] Here, $\text{stdBasisMatrix}\, i\, j\, c$ denotes the matrix with entry $c$ at position $(i, j)$ and zeros elsewhere.
Matrix.StdBasisMatrix.mul_of_ne theorem
(i : l) (j k : m) {l : n} (h : j ≠ k) (d : α) : stdBasisMatrix i j c * stdBasisMatrix k l d = 0
Full source 
@[simp]
theorem mul_of_ne (i : l) (j k : m) {l : n} (h : j ≠ k) (d : α) :
    stdBasisMatrix i j c * stdBasisMatrix k l d = 0 := by
  ext a b
  simp only [mul_apply, boole_mul, stdBasisMatrix, of_apply]
  by_cases h₁ : i = a
  · simp [h₁, h, Finset.sum_eq_zero]
  · simp [h₁]
Product of Standard Basis Matrices with Non-Matching Indices is Zero
Informal description
For any row indices $i \in l$, column indices $j, k \in m$ with $j \neq k$, and any column index $l \in n$, the product of the standard basis matrices $\text{stdBasisMatrix}\, i\, j\, c$ and $\text{stdBasisMatrix}\, k\, l\, d$ is the zero matrix. That is, $\text{stdBasisMatrix}\, i\, j\, c \cdot \text{stdBasisMatrix}\, k\, l\, d = 0$.
Matrix.row_eq_zero_of_commute_stdBasisMatrix theorem
{i j k : n} {M : Matrix n n α} (hM : Commute (stdBasisMatrix i j 1) M) (hkj : k ≠ j) : M j k = 0
Full source 
theorem row_eq_zero_of_commute_stdBasisMatrix {i j k : n} {M : Matrix n n α}
    (hM : Commute (stdBasisMatrix i j 1) M) (hkj : k ≠ j) : M j k = 0 := by
  have := ext_iff.mpr hM i k
  aesop
Vanishing of Matrix Entry under Commutation with Standard Basis Matrix
Informal description
Let $M$ be an $n \times n$ matrix over a type $\alpha$, and let $i, j, k$ be indices in $n$ such that $k \neq j$. If the standard basis matrix $\text{stdBasisMatrix}\, i\, j\, 1$ commutes with $M$, then the $(j, k)$-th entry of $M$ is zero, i.e., $M_{j,k} = 0$.
Matrix.col_eq_zero_of_commute_stdBasisMatrix theorem
{i j k : n} {M : Matrix n n α} (hM : Commute (stdBasisMatrix i j 1) M) (hki : k ≠ i) : M k i = 0
Full source 
theorem col_eq_zero_of_commute_stdBasisMatrix {i j k : n} {M : Matrix n n α}
    (hM : Commute (stdBasisMatrix i j 1) M) (hki : k ≠ i) : M k i = 0 := by
  have := ext_iff.mpr hM k j
  aesop
Vanishing Column Entries under Commutation with Standard Basis Matrix
Informal description
For any square matrix $M$ of size $n \times n$ with entries in type $\alpha$, and for any indices $i, j, k \in n$ with $k \neq i$, if the standard basis matrix $\text{stdBasisMatrix}(i, j, 1)$ commutes with $M$, then the $(k, i)$-entry of $M$ is zero, i.e., $M_{k,i} = 0$.
Matrix.diag_eq_of_commute_stdBasisMatrix theorem
{i j : n} {M : Matrix n n α} (hM : Commute (stdBasisMatrix i j 1) M) : M i i = M j j
Full source 
theorem diag_eq_of_commute_stdBasisMatrix {i j : n} {M : Matrix n n α}
    (hM : Commute (stdBasisMatrix i j 1) M) : M i i = M j j := by
  have := ext_iff.mpr hM i j
  aesop
Equality of Diagonal Entries under Commutation with Standard Basis Matrix
Informal description
For any square matrix $M$ of size $n \times n$ with entries in type $\alpha$, and for any indices $i, j \in n$, if the standard basis matrix $\text{stdBasisMatrix}(i, j, 1)$ commutes with $M$, then the diagonal entries of $M$ at positions $(i, i)$ and $(j, j)$ are equal, i.e., $M_{i,i} = M_{j,j}$.
Matrix.mem_range_scalar_of_commute_stdBasisMatrix theorem
{M : Matrix n n α} (hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M) : M ∈ Set.range (Matrix.scalar n)
Full source 
/-- `M` is a scalar matrix if it commutes with every non-diagonal `stdBasisMatrix`. -/
theorem mem_range_scalar_of_commute_stdBasisMatrix {M : Matrix n n α}
    (hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M) :
    M ∈ Set.range (Matrix.scalar n) := by
  cases isEmpty_or_nonempty n
  · exact ⟨0, Subsingleton.elim _ _⟩
  obtain ⟨i⟩ := ‹Nonempty n›
  refine ⟨M i i, Matrix.ext fun j k => ?_⟩
  simp only [scalar_apply]
  obtain rfl | hkl := Decidable.eq_or_ne j k
  · rw [diagonal_apply_eq]
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rfl
    · exact diag_eq_of_commute_stdBasisMatrix (hM hij)
  · rw [diagonal_apply_ne _ hkl]
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [col_eq_zero_of_commute_stdBasisMatrix (hM hkl.symm) hkl]
    · rw [row_eq_zero_of_commute_stdBasisMatrix (hM hij) hkl.symm]
Scalar Matrix Characterization via Commutation with Standard Basis Matrices
Informal description
Let $M$ be an $n \times n$ matrix over a type $\alpha$. If $M$ commutes with every standard basis matrix $\text{stdBasisMatrix}(i, j, 1)$ for all distinct indices $i, j \in n$, then $M$ is a scalar matrix, i.e., there exists a scalar $c \in \alpha$ such that $M = c I_n$, where $I_n$ is the identity matrix of size $n \times n$.
Matrix.mem_range_scalar_iff_commute_stdBasisMatrix theorem
{M : Matrix n n α} : M ∈ Set.range (Matrix.scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M
Full source 
theorem mem_range_scalar_iff_commute_stdBasisMatrix {M : Matrix n n α} :
    M ∈ Set.range (Matrix.scalar n)M ∈ Set.range (Matrix.scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M := by
  refine ⟨fun ⟨r, hr⟩ i j _ => hr ▸ Commute.symm ?_, mem_range_scalar_of_commute_stdBasisMatrix⟩
  rw [scalar_commute_iff]
  simp
Characterization of Scalar Matrices via Commutation with Standard Basis Matrices
Informal description
For any square matrix $M$ of size $n \times n$ with entries in type $\alpha$, the following are equivalent: 1. $M$ is a scalar matrix, i.e., there exists a scalar $c \in \alpha$ such that $M = c I_n$ where $I_n$ is the identity matrix. 2. For all distinct indices $i, j \in n$, the standard basis matrix $\text{stdBasisMatrix}(i, j, 1)$ commutes with $M$. Here, $\text{stdBasisMatrix}(i, j, 1)$ denotes the matrix with entry $1$ at position $(i,j)$ and zeros elsewhere.
Matrix.mem_range_scalar_iff_commute_stdBasisMatrix' theorem
{M : Matrix n n α} : M ∈ Set.range (Matrix.scalar n) ↔ ∀ (i j : n), Commute (stdBasisMatrix i j 1) M
Full source 
/-- `M` is a scalar matrix if and only if it commutes with every `stdBasisMatrix`. -/
theorem mem_range_scalar_iff_commute_stdBasisMatrix' {M : Matrix n n α} :
    M ∈ Set.range (Matrix.scalar n)M ∈ Set.range (Matrix.scalar n) ↔ ∀ (i j : n), Commute (stdBasisMatrix i j 1) M := by
  refine ⟨fun ⟨r, hr⟩ i j => hr ▸ Commute.symm ?_,
    fun hM => mem_range_scalar_iff_commute_stdBasisMatrix.mpr <| fun i j _ => hM i j⟩
  rw [scalar_commute_iff]
  simp
Characterization of Scalar Matrices via Commutation with All Standard Basis Matrices
Informal description
For any square matrix $M$ of size $n \times n$ with entries in a type $\alpha$, the following are equivalent: 1. $M$ is a scalar matrix, i.e., there exists a scalar $c \in \alpha$ such that $M = c I_n$ where $I_n$ is the identity matrix. 2. For all indices $i, j \in n$, the standard basis matrix $\text{stdBasisMatrix}(i, j, 1)$ commutes with $M$. Here, $\text{stdBasisMatrix}(i, j, 1)$ denotes the matrix with entry $1$ at position $(i,j)$ and zeros elsewhere.