doc-next-gen

Mathlib.Data.Matrix.Diagonal

Module docstring

{"# Diagonal matrices

This file defines diagonal matrices and the AddCommMonoidWithOne structure on matrices.

Main definitions

  • Matrix.diagonal d: matrix with the vector d along the diagonal
  • Matrix.diag M: the diagonal of a square matrix
  • Matrix.instAddCommMonoidWithOne: matrices are an additive commutative monoid with one ","simp lemmas for Matrix.submatrixs interaction with Matrix.diagonal, 1, and Matrix.mul for when the mappings are bundled. "}
Matrix.diagonal definition
[Zero α] (d : n → α) : Matrix n n α
Full source 
/-- `diagonal d` is the square matrix such that `(diagonal d) i i = d i` and `(diagonal d) i j = 0`
if `i ≠ j`.

Note that bundled versions exist as:
* `Matrix.diagonalAddMonoidHom`
* `Matrix.diagonalLinearMap`
* `Matrix.diagonalRingHom`
* `Matrix.diagonalAlgHom`
-/
def diagonal [Zero α] (d : n → α) : Matrix n n α :=
  of fun i j => if i = j then d i else 0
Diagonal matrix construction
Informal description
Given a type `n` and a zero element for type `α`, the function `diagonal` maps a vector `d : n → α` to a square matrix of size `n × n` with entries `d i` on the diagonal and zero elsewhere. Specifically, for indices `i` and `j`, the matrix entry at position `(i, j)` is `d i` if `i = j` and `0` otherwise.
Matrix.diagonal_apply theorem
[Zero α] (d : n → α) (i j) : diagonal d i j = if i = j then d i else 0
Full source 
theorem diagonal_apply [Zero α] (d : n → α) (i j) : diagonal d i j = if i = j then d i else 0 :=
  rfl
Definition of Diagonal Matrix Entries
Informal description
Given a type `n` with a zero element for type `α`, a vector `d : n → α`, and indices `i, j : n`, the entry of the diagonal matrix at position `(i, j)` is defined as: \[ (\text{diagonal } d)_{i,j} = \begin{cases} d_i & \text{if } i = j, \\ 0 & \text{otherwise.} \end{cases} \]
Matrix.diagonal_apply_eq theorem
[Zero α] (d : n → α) (i : n) : (diagonal d) i i = d i
Full source 
@[simp]
theorem diagonal_apply_eq [Zero α] (d : n → α) (i : n) : (diagonal d) i i = d i := by
  simp [diagonal]
Diagonal Matrix Entry at $(i,i)$ Equals $d_i$
Informal description
For any type `n` with a zero element of type `α`, given a vector `d : n → α` and an index `i : n`, the diagonal entry at position `(i, i)` of the matrix constructed by `diagonal d` is equal to `d i`. That is, $(\text{diagonal } d)_{i,i} = d_i$.
Matrix.diagonal_apply_ne theorem
[Zero α] (d : n → α) {i j : n} (h : i ≠ j) : (diagonal d) i j = 0
Full source 
@[simp]
theorem diagonal_apply_ne [Zero α] (d : n → α) {i j : n} (h : i ≠ j) : (diagonal d) i j = 0 := by
  simp [diagonal, h]
Off-diagonal entries of a diagonal matrix are zero
Informal description
For any type `n` with a zero element of type `α`, given a vector `d : n → α` and distinct indices `i, j : n`, the entry at position `(i, j)` of the diagonal matrix constructed from `d` is zero. That is, if $i \neq j$, then $(\text{diagonal } d)_{i,j} = 0$.
Matrix.diagonal_apply_ne' theorem
[Zero α] (d : n → α) {i j : n} (h : j ≠ i) : (diagonal d) i j = 0
Full source 
theorem diagonal_apply_ne' [Zero α] (d : n → α) {i j : n} (h : j ≠ i) : (diagonal d) i j = 0 :=
  diagonal_apply_ne d h.symm
Off-diagonal entries of a diagonal matrix vanish when $j \neq i$
Informal description
For any type `n` with a zero element of type `α`, given a vector `d : n → α` and distinct indices `i, j : n` such that $j \neq i$, the entry at position $(i, j)$ of the diagonal matrix constructed from `d` is zero. That is, $(\text{diagonal } d)_{i,j} = 0$.
Matrix.diagonal_eq_diagonal_iff theorem
[Zero α] {d₁ d₂ : n → α} : diagonal d₁ = diagonal d₂ ↔ ∀ i, d₁ i = d₂ i
Full source 
@[simp]
theorem diagonal_eq_diagonal_iff [Zero α] {d₁ d₂ : n → α} :
    diagonaldiagonal d₁ = diagonal d₂ ↔ ∀ i, d₁ i = d₂ i :=
  ⟨fun h i => by simpa using congr_arg (fun m : Matrix n n α => m i i) h, fun h => by
    rw [show d₁ = d₂ from funext h]⟩
Equality of Diagonal Matrices is Equivalent to Equality of Diagonal Entries
Informal description
For any type `n` with a zero element of type `α`, and for any two vectors `d₁, d₂ : n → α`, the diagonal matrices constructed from `d₁` and `d₂` are equal if and only if `d₁ i = d₂ i` for all indices `i : n`. That is, $\text{diagonal}(d₁) = \text{diagonal}(d₂) \leftrightarrow \forall i, d₁ i = d₂ i$.
Matrix.diagonal_injective theorem
[Zero α] : Function.Injective (diagonal : (n → α) → Matrix n n α)
Full source 
theorem diagonal_injective [Zero α] : Function.Injective (diagonal : (n → α) → Matrix n n α) :=
  fun d₁ d₂ h => funext fun i => by simpa using Matrix.ext_iff.mpr h i i
Injectivity of Diagonal Matrix Construction
Informal description
For any type `n` and any type `α` with a zero element, the function that constructs a diagonal matrix from a vector `d : n → α` is injective. That is, if two diagonal matrices are equal, then their corresponding diagonal vectors must be equal.
Matrix.diagonal_zero theorem
[Zero α] : (diagonal fun _ => 0 : Matrix n n α) = 0
Full source 
@[simp]
theorem diagonal_zero [Zero α] : (diagonal fun _ => 0 : Matrix n n α) = 0 := by
  ext
  simp [diagonal]
Diagonal Matrix of Zeros is the Zero Matrix
Informal description
For any type `n` and any type `α` with a zero element, the diagonal matrix constructed from the constant zero function is equal to the zero matrix. That is, $\text{diagonal}(\lambda \_, 0) = 0$.
Matrix.diagonal_transpose theorem
[Zero α] (v : n → α) : (diagonal v)ᵀ = diagonal v
Full source 
@[simp]
theorem diagonal_transpose [Zero α] (v : n → α) : (diagonal v)ᵀ = diagonal v := by
  ext i j
  by_cases h : i = j
  · simp [h, transpose]
  · simp [h, transpose, diagonal_apply_ne' _ h]
Transpose of Diagonal Matrix is Diagonal
Informal description
For any type `n` and any type `α` with a zero element, the transpose of a diagonal matrix constructed from a vector $v : n \to \alpha$ is equal to the diagonal matrix itself. That is, $(\text{diagonal } v)^\top = \text{diagonal } v$.
Matrix.diagonal_add theorem
[AddZeroClass α] (d₁ d₂ : n → α) : diagonal d₁ + diagonal d₂ = diagonal fun i => d₁ i + d₂ i
Full source 
@[simp]
theorem diagonal_add [AddZeroClass α] (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]
Additivity of Diagonal Matrix Construction
Informal description
For any type `n` and any type `α` with an additive structure and a zero element, given two vectors `d₁, d₂ : n → α`, the sum of the diagonal matrices constructed from `d₁` and `d₂` is equal to the diagonal matrix constructed from the pointwise sum of `d₁` and `d₂`. That is, $$\text{diagonal}(d₁) + \text{diagonal}(d₂) = \text{diagonal}(\lambda i, d₁_i + d₂_i).$$
Matrix.diagonal_smul theorem
[Zero α] [SMulZeroClass R α] (r : R) (d : n → α) : diagonal (r • d) = r • diagonal d
Full source 
@[simp]
theorem diagonal_smul [Zero α] [SMulZeroClass R α] (r : R) (d : n → α) :
    diagonal (r • d) = r • diagonal d := by
  ext i j
  by_cases h : i = j <;> simp [h]
Scalar Multiplication Commutes with Diagonal Matrix Construction
Informal description
Let $R$ be a type with a scalar multiplication operation $\cdot : R \times \alpha \to \alpha$ where $\alpha$ has a zero element. For any scalar $r \in R$ and vector $d : n \to \alpha$, the diagonal matrix constructed from the scaled vector $r \cdot d$ is equal to the scalar multiple $r \cdot (\text{diagonal } d)$. That is, $$\text{diagonal}(r \cdot d) = r \cdot \text{diagonal}(d).$$
Matrix.diagonal_neg theorem
[NegZeroClass α] (d : n → α) : -diagonal d = diagonal fun i => -d i
Full source 
@[simp]
theorem diagonal_neg [NegZeroClass α] (d : n → α) :
    -diagonal d = diagonal fun i => -d i := by
  ext i j
  by_cases h : i = j <;>
  simp [h]
Negation of Diagonal Matrix Equals Diagonal of Negations
Informal description
For any type `n` and any type `α` with a negation operation and a zero element, given a vector `d : n → α`, the negation of the diagonal matrix constructed from `d` is equal to the diagonal matrix constructed from the pointwise negation of `d`. That is, $$- \text{diagonal}(d) = \text{diagonal}(\lambda i, -d_i).$$
Matrix.diagonal_sub theorem
[SubNegZeroMonoid α] (d₁ d₂ : n → α) : diagonal d₁ - diagonal d₂ = diagonal fun i => d₁ i - d₂ i
Full source 
@[simp]
theorem diagonal_sub [SubNegZeroMonoid α] (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]
Difference of Diagonal Matrices Equals Diagonal of Differences
Informal description
Let $\alpha$ be a type with subtraction and a zero element, and let $d_1, d_2 : n \to \alpha$ be two vectors. The difference of the diagonal matrices constructed from $d_1$ and $d_2$ is equal to the diagonal matrix constructed from the pointwise difference of $d_1$ and $d_2$. That is, $$\text{diagonal}(d_1) - \text{diagonal}(d_2) = \text{diagonal}(\lambda i, d_1(i) - d_2(i)).$$
Matrix.instNatCastOfZero instance
[Zero α] [NatCast α] : NatCast (Matrix n n α)
Full source 
instance [Zero α] [NatCast α] : NatCast (Matrix n n α) where
  natCast m := diagonal fun _ => m
Natural Number Casting for Square Matrices
Informal description
For any type `n` and type `α` with a zero element and a natural number casting operation, the square matrices of size `n × n` with entries in `α` inherit a natural number casting operation. Specifically, the natural number `m` is cast to the diagonal matrix with `m` (as an element of `α`) on every diagonal entry and zero elsewhere.
Matrix.diagonal_natCast theorem
[Zero α] [NatCast α] (m : ℕ) : diagonal (fun _ : n => (m : α)) = m
Full source 
@[norm_cast]
theorem diagonal_natCast [Zero α] [NatCast α] (m : ℕ) : diagonal (fun _ : n => (m : α)) = m := rfl
Diagonal Matrix from Constant Function Equals Natural Number Cast
Informal description
For any type $\alpha$ with a zero element and a natural number casting operation, and for any natural number $m$, the diagonal matrix constructed from the constant function mapping every index to $m$ (as an element of $\alpha$) is equal to the natural number $m$ cast as a matrix. That is, $\text{diagonal}(\lambda \_, m) = m$ as matrices.
Matrix.diagonal_natCast' theorem
[Zero α] [NatCast α] (m : ℕ) : diagonal ((m : n → α)) = m
Full source 
@[norm_cast]
theorem diagonal_natCast' [Zero α] [NatCast α] (m : ℕ) : diagonal ((m : n → α)) = m := rfl
Diagonal Matrix from Constant Function Equals Natural Number Cast
Informal description
For any type `α` with a zero element and a natural number casting operation, and for any natural number `m`, the diagonal matrix constructed from the constant function `n → α` mapping every index to `m` is equal to the natural number `m` cast as a matrix.
Matrix.diagonal_ofNat theorem
[Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] : diagonal (fun _ : n => (ofNat(m) : α)) = OfNat.ofNat m
Full source 
theorem diagonal_ofNat [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] :
    diagonal (fun _ : n => (ofNat(m) : α)) = OfNat.ofNat m := rfl
Diagonal Matrix from Constant Function Equals Natural Number Cast for $m \geq 2$
Informal description
For any type $\alpha$ with a zero element and a natural number casting operation, and for any natural number $m \geq 2$, the diagonal matrix constructed from the constant function $n \to \alpha$ mapping every index to $m$ is equal to the natural number $m$ cast as a matrix. That is, $\text{diagonal}(\lambda \_, m) = m$ as matrices.
Matrix.diagonal_ofNat' theorem
[Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] : diagonal (ofNat(m) : n → α) = OfNat.ofNat m
Full source 
theorem diagonal_ofNat' [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] :
    diagonal (ofNat(m) : n → α) = OfNat.ofNat m := rfl
Diagonal Matrix from Constant Function Equals Scalar Matrix for $m \geq 2$
Informal description
For any type $\alpha$ with a zero element and a natural number casting operation, and for any natural number $m \geq 2$, the diagonal matrix constructed from the constant function mapping every index to $m$ (as an element of $\alpha$) is equal to the matrix representation of $m$ (i.e., the scalar matrix with $m$ on the diagonal and zeros elsewhere). In other words, $\text{diagonal}(\lambda \_, m) = mI$, where $I$ is the identity matrix.
Matrix.instIntCastOfZero instance
[Zero α] [IntCast α] : IntCast (Matrix n n α)
Full source 
instance [Zero α] [IntCast α] : IntCast (Matrix n n α) where
  intCast m := diagonal fun _ => m
Integer Casting for Square Matrices
Informal description
For any type `n` and type `α` with a zero element and integer casting operation, the space of square matrices `n × n` over `α` inherits an integer casting operation.
Matrix.diagonal_intCast theorem
[Zero α] [IntCast α] (m : ℤ) : diagonal (fun _ : n => (m : α)) = m
Full source 
@[norm_cast]
theorem diagonal_intCast [Zero α] [IntCast α] (m : ℤ) : diagonal (fun _ : n => (m : α)) = m := rfl
Diagonal Matrix of Constant Integer Function Equals Scalar Matrix
Informal description
For any type $\alpha$ with a zero element and integer casting operation, and for any integer $m$, the diagonal matrix with all diagonal entries equal to $m$ (interpreted as an element of $\alpha$) is equal to the scalar matrix $m$ (where $m$ is interpreted as a matrix with $m$ on the diagonal and zeros elsewhere). In other words, if $d$ is the constant function mapping every index to $m$, then $\text{diagonal}(d) = mI$, where $I$ is the identity matrix.
Matrix.diagonal_intCast' theorem
[Zero α] [IntCast α] (m : ℤ) : diagonal ((m : n → α)) = m
Full source 
@[norm_cast]
theorem diagonal_intCast' [Zero α] [IntCast α] (m : ℤ) : diagonal ((m : n → α)) = m := rfl
Diagonal Matrix of Constant Integer Function Equals Scalar Matrix
Informal description
For any type `α` with a zero element and integer casting operation, and for any integer `m`, the diagonal matrix constructed from the constant function `n → α` mapping every index to `m` is equal to the scalar matrix `m` (interpreted as a matrix with `m` on the diagonal and zeros elsewhere). In other words, the diagonal matrix with all diagonal entries equal to `m` is equal to the matrix `mI`, where `I` is the identity matrix.
Matrix.diagonal_map theorem
[Zero α] [Zero β] {f : α → β} (h : f 0 = 0) {d : n → α} : (diagonal d).map f = diagonal fun m => f (d m)
Full source 
@[simp]
theorem diagonal_map [Zero α] [Zero β] {f : α → β} (h : f 0 = 0) {d : n → α} :
    (diagonal d).map f = diagonal fun m => f (d m) := by
  ext
  simp only [diagonal_apply, map_apply]
  split_ifs <;> simp [h]
Mapping Preserves Diagonal Matrix Construction
Informal description
Let $\alpha$ and $\beta$ be types with zero elements, and let $f : \alpha \to \beta$ be a function such that $f(0) = 0$. For any vector $d : n \to \alpha$, the map of the diagonal matrix constructed from $d$ under $f$ is equal to the diagonal matrix constructed from the vector $f \circ d$. In other words, $$(\text{diagonal } d).\text{map } f = \text{diagonal } (f \circ d).$$
Matrix.map_natCast theorem
[AddMonoidWithOne α] [Zero β] {f : α → β} (h : f 0 = 0) (d : ℕ) : (d : Matrix n n α).map f = diagonal (fun _ => f d)
Full source 
protected theorem map_natCast [AddMonoidWithOne α] [Zero β]
    {f : α → β} (h : f 0 = 0) (d : ℕ) :
    (d : Matrix n n α).map f = diagonal (fun _ => f d) :=
  diagonal_map h
Mapping Preserves Diagonal Matrix of Natural Number $d$
Informal description
Let $\alpha$ be a type with an additive monoid structure with one, $\beta$ a type with a zero element, and $f : \alpha \to \beta$ a function such that $f(0) = 0$. For any natural number $d$, the map of the diagonal matrix with all diagonal entries equal to $d$ (as an element of $\alpha$) under $f$ is equal to the diagonal matrix with all diagonal entries equal to $f(d)$. In other words, $$f(dI_n) = \text{diag}(f(d), \dots, f(d)),$$ where $I_n$ is the $n \times n$ identity matrix with diagonal entries $d$.
Matrix.map_ofNat theorem
[AddMonoidWithOne α] [Zero β] {f : α → β} (h : f 0 = 0) (d : ℕ) [d.AtLeastTwo] : (ofNat(d) : Matrix n n α).map f = diagonal (fun _ => f (OfNat.ofNat d))
Full source 
protected theorem map_ofNat [AddMonoidWithOne α] [Zero β]
    {f : α → β} (h : f 0 = 0) (d : ℕ) [d.AtLeastTwo] :
    (ofNat(d) : Matrix n n α).map f = diagonal (fun _ => f (OfNat.ofNat d)) :=
  diagonal_map h
Mapping Preserves Diagonal Matrix of Natural Number $d \geq 2$
Informal description
Let $\alpha$ be a type with an additive monoid structure with one, $\beta$ a type with a zero element, and $f : \alpha \to \beta$ a function such that $f(0) = 0$. For any natural number $d \geq 2$, the map of the diagonal matrix with all diagonal entries equal to $d$ (as an element of $\alpha$) under $f$ is equal to the diagonal matrix with all diagonal entries equal to $f(d)$. In other words, $$f(dI_n) = \text{diag}(f(d), \dots, f(d)),$$ where $I_n$ is the $n \times n$ identity matrix with diagonal entries $d$.
Matrix.map_intCast theorem
[AddGroupWithOne α] [Zero β] {f : α → β} (h : f 0 = 0) (d : ℤ) : (d : Matrix n n α).map f = diagonal (fun _ => f d)
Full source 
protected theorem map_intCast [AddGroupWithOne α] [Zero β]
    {f : α → β} (h : f 0 = 0) (d : ℤ) :
    (d : Matrix n n α).map f = diagonal (fun _ => f d) :=
  diagonal_map h
Mapping Preserves Diagonal Matrix of Integer $d$
Informal description
Let $\alpha$ be a type with an additive group structure with one, $\beta$ a type with a zero element, and $f : \alpha \to \beta$ a function such that $f(0) = 0$. For any integer $d$, the map of the diagonal matrix with all diagonal entries equal to $d$ (as an element of $\alpha$) under $f$ is equal to the diagonal matrix with all diagonal entries equal to $f(d)$. In other words, $$f(dI_n) = \text{diag}(f(d), \dots, f(d)),$$ where $I_n$ is the $n \times n$ identity matrix with diagonal entries $d$.
Matrix.diagonal_unique theorem
[Unique m] [DecidableEq m] [Zero α] (d : m → α) : diagonal d = of fun _ _ => d default
Full source 
theorem diagonal_unique [Unique m] [DecidableEq m] [Zero α] (d : m → α) :
    diagonal d = of fun _ _ => d default := by
  ext i j
  rw [Subsingleton.elim i default, Subsingleton.elim j default, diagonal_apply_eq _ _, of_apply]
Diagonal Matrix Equality for Unique Index Type
Informal description
For a unique type `m` with decidable equality and a type `α` with a zero element, given a vector `d : m → α`, the diagonal matrix constructed from `d` is equal to the matrix where every entry is `d default`. Here, `default` refers to the unique element of the type `m`. In other words, if `m` has exactly one element, then the diagonal matrix with diagonal entries `d` is the same as the constant matrix where every entry is `d` evaluated at the unique element of `m`.
Matrix.one instance
: One (Matrix n n α)
Full source 
instance one : One (Matrix n n α) :=
  ⟨diagonal fun _ => 1⟩
Identity Matrix as One Element in Square Matrices
Informal description
For any type `n` and any type `α` with a one element, the square matrices of size `n × n` over `α` have a one element given by the identity matrix, where the diagonal entries are `1` and the off-diagonal entries are `0`.
Matrix.diagonal_one theorem
: (diagonal fun _ => 1 : Matrix n n α) = 1
Full source 
@[simp]
theorem diagonal_one : (diagonal fun _ => 1 : Matrix n n α) = 1 :=
  rfl
Diagonal Matrix of Ones Equals Identity Matrix
Informal description
The diagonal matrix with all diagonal entries equal to $1$ is equal to the identity matrix of size $n \times n$ over a type $\alpha$ with a multiplicative identity, i.e., $\text{diagonal}(\lambda \_, 1) = 1$.
Matrix.one_apply theorem
{i j} : (1 : Matrix n n α) i j = if i = j then 1 else 0
Full source 
theorem one_apply {i j} : (1 : Matrix n n α) i j = if i = j then 1 else 0 :=
  rfl
Entrywise Definition of Identity Matrix
Informal description
For any indices $i$ and $j$ in a square matrix of size $n \times n$ over a type $\alpha$ with a multiplicative identity, the $(i,j)$-th entry of the identity matrix is $1$ if $i = j$ and $0$ otherwise, i.e., $$(1 : \text{Matrix } n n \alpha)_{i,j} = \begin{cases} 1 & \text{if } i = j, \\ 0 & \text{otherwise.} \end{cases}$$
Matrix.one_apply_eq theorem
(i) : (1 : Matrix n n α) i i = 1
Full source 
@[simp]
theorem one_apply_eq (i) : (1 : Matrix n n α) i i = 1 :=
  diagonal_apply_eq _ i
Diagonal Entry of Identity Matrix Equals One
Informal description
For any type `n` and any type `α` with a multiplicative identity element, the diagonal entry at position $(i, i)$ of the identity matrix of size $n \times n$ over $\alpha$ is equal to $1$, i.e., $(1 : \text{Matrix } n n \alpha)_{i,i} = 1$.
Matrix.one_apply_ne theorem
{i j} : i ≠ j → (1 : Matrix n n α) i j = 0
Full source 
@[simp]
theorem one_apply_ne {i j} : i ≠ j → (1 : Matrix n n α) i j = 0 :=
  diagonal_apply_ne _
Off-diagonal entries of identity matrix are zero
Informal description
For any indices $i$ and $j$ in a square matrix of size $n \times n$ over a type $\alpha$ with a multiplicative identity, if $i \neq j$, then the $(i,j)$-th entry of the identity matrix is $0$, i.e., $$(1 : \text{Matrix } n n \alpha)_{i,j} = 0 \quad \text{when } i \neq j.$$
Matrix.one_apply_ne' theorem
{i j} : j ≠ i → (1 : Matrix n n α) i j = 0
Full source 
theorem one_apply_ne' {i j} : j ≠ i → (1 : Matrix n n α) i j = 0 :=
  diagonal_apply_ne' _
Off-diagonal entries of identity matrix vanish when $j \neq i$
Informal description
For any indices $i$ and $j$ in a square matrix of size $n \times n$ over a type $\alpha$ with a multiplicative identity, if $j \neq i$, then the $(i,j)$-th entry of the identity matrix is $0$, i.e., $$(1 : \text{Matrix } n n \alpha)_{i,j} = 0 \quad \text{when } j \neq i.$$
Matrix.map_one theorem
[Zero β] [One β] (f : α → β) (h₀ : f 0 = 0) (h₁ : f 1 = 1) : (1 : Matrix n n α).map f = (1 : Matrix n n β)
Full source 
@[simp]
protected theorem map_one [Zero β] [One β] (f : α → β) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
    (1 : Matrix n n α).map f = (1 : Matrix n n β) := by
  ext
  simp only [one_apply, map_apply]
  split_ifs <;> simp [h₀, h₁]
Mapping Preserves Identity Matrix under Zero and One Conditions
Informal description
Let $n$ be a type, and let $\alpha$ and $\beta$ be types equipped with zero and one elements. Given a function $f : \alpha \to \beta$ such that $f(0) = 0$ and $f(1) = 1$, the mapping of the identity matrix in $\text{Matrix}(n, n, \alpha)$ under $f$ is equal to the identity matrix in $\text{Matrix}(n, n, \beta)$. That is, $(1 : \text{Matrix}(n, n, \alpha)).\text{map}(f) = (1 : \text{Matrix}(n, n, \beta))$.
Matrix.one_eq_pi_single theorem
{i j} : (1 : Matrix n n α) i j = Pi.single (f := fun _ => α) i 1 j
Full source 
theorem one_eq_pi_single {i j} : (1 : Matrix n n α) i j = Pi.single (f := fun _ => α) i 1 j := by
  simp only [one_apply, Pi.single_apply, eq_comm]
Identity Matrix as Pointwise Single Function
Informal description
For any indices $i$ and $j$, the $(i,j)$-th entry of the identity matrix in $\text{Matrix}(n, n, \alpha)$ is equal to the value of the function $\text{Pi.single}_i(1)$ evaluated at $j$, where $\text{Pi.single}_i(1)$ is the function that takes the value $1$ at $i$ and $0$ elsewhere.
Matrix.instAddMonoidWithOne instance
[AddMonoidWithOne α] : AddMonoidWithOne (Matrix n n α)
Full source 
instance instAddMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (Matrix n n α) where
  natCast_zero := show diagonal _ = _ by
    rw [Nat.cast_zero, diagonal_zero]
  natCast_succ n := show diagonal _ = diagonal _ + _ by
    rw [Nat.cast_succ, ← diagonal_add, diagonal_one]
Additive Monoid with One Structure on Square Matrices
Informal description
For any type `n` and any type `α` that is an additive monoid with one, the square matrices of size `n × n` with entries in `α` form an additive monoid with one. The zero matrix serves as the additive identity, and the identity matrix (with ones on the diagonal and zeros elsewhere) serves as the multiplicative identity.
Matrix.instAddGroupWithOne instance
[AddGroupWithOne α] : AddGroupWithOne (Matrix n n α)
Full source 
instance instAddGroupWithOne [AddGroupWithOne α] : AddGroupWithOne (Matrix n n α) where
  intCast_ofNat n := show diagonal _ = diagonal _ by
    rw [Int.cast_natCast]
  intCast_negSucc n := show diagonal _ = -(diagonal _) by
    rw [Int.cast_negSucc, diagonal_neg]
  __ := addGroup
  __ := instAddMonoidWithOne
Additive Group with One Structure on Square Matrices
Informal description
For any type `n` and any type `α` that is an additive group with one, the square matrices of size `n × n` with entries in `α` form an additive group with one. This includes the operations of matrix addition, negation, and the identity matrix.
Matrix.instAddCommMonoidWithOne instance
[AddCommMonoidWithOne α] : AddCommMonoidWithOne (Matrix n n α)
Full source 
instance instAddCommMonoidWithOne [AddCommMonoidWithOne α] :
    AddCommMonoidWithOne (Matrix n n α) where
  __ := addCommMonoid
  __ := instAddMonoidWithOne
Additive Commutative Monoid with One Structure on Square Matrices
Informal description
For any type `n` and any type `α` that is an additive commutative monoid with one, the square matrices of size `n × n` with entries in `α` form an additive commutative monoid with one. The zero matrix serves as the additive identity, and the identity matrix (with ones on the diagonal and zeros elsewhere) serves as the multiplicative identity.
Matrix.instAddCommGroupWithOne instance
[AddCommGroupWithOne α] : AddCommGroupWithOne (Matrix n n α)
Full source 
instance instAddCommGroupWithOne [AddCommGroupWithOne α] :
    AddCommGroupWithOne (Matrix n n α) where
  __ := addCommGroup
  __ := instAddGroupWithOne
Additive Commutative Group with One Structure on Square Matrices
Informal description
For any type `n` and any type `α` that is an additive commutative group with one, the square matrices of size `n × n` with entries in `α` form an additive commutative group with one. This includes the operations of matrix addition, negation, and the identity matrix, with addition being commutative.
Matrix.diag definition
(A : Matrix n n α) (i : n) : α
Full source 
/-- The diagonal of a square matrix. -/
def diag (A : Matrix n n α) (i : n) : α :=
  A i i
Diagonal of a square matrix
Informal description
The function that extracts the diagonal elements of a square matrix $A$ of size $n \times n$ over a type $\alpha$. For each index $i$, the value $\text{diag}(A)(i)$ is equal to the $(i,i)$-th entry of $A$.
Matrix.diag_apply theorem
(A : Matrix n n α) (i) : diag A i = A i i
Full source 
@[simp]
theorem diag_apply (A : Matrix n n α) (i) : diag A i = A i i :=
  rfl
Diagonal Element Equals Matrix Entry: $\text{diag}(A)(i) = A_{i,i}$
Informal description
For any square matrix $A$ of size $n \times n$ over a type $\alpha$ and any index $i$, the $i$-th diagonal element of $A$ is equal to the $(i,i)$-th entry of $A$, i.e., $\text{diag}(A)(i) = A_{i,i}$.
Matrix.diag_diagonal theorem
[DecidableEq n] [Zero α] (a : n → α) : diag (diagonal a) = a
Full source 
@[simp]
theorem diag_diagonal [DecidableEq n] [Zero α] (a : n → α) : diag (diagonal a) = a :=
  funext <| @diagonal_apply_eq _ _ _ _ a
Diagonal Extraction from Diagonal Matrix: $\text{diag}(\text{diag}(a)) = a$
Informal description
For any type `n` with decidable equality and any type `α` with a zero element, given a vector `a : n → α`, the diagonal of the matrix `diagonal a` is equal to `a`. That is, $\text{diag}(\text{diagonal } a) = a$.
Matrix.diag_transpose theorem
(A : Matrix n n α) : diag Aᵀ = diag A
Full source 
@[simp]
theorem diag_transpose (A : Matrix n n α) : diag Aᵀ = diag A :=
  rfl
Diagonal Invariance Under Matrix Transposition
Informal description
For any square matrix $A$ of size $n \times n$ over a type $\alpha$, the diagonal of its transpose $A^\top$ is equal to the diagonal of $A$, i.e., $\text{diag}(A^\top) = \text{diag}(A)$.
Matrix.diag_zero theorem
[Zero α] : diag (0 : Matrix n n α) = 0
Full source 
@[simp]
theorem diag_zero [Zero α] : diag (0 : Matrix n n α) = 0 :=
  rfl
Diagonal of Zero Matrix is Zero Function
Informal description
For any type $\alpha$ with a zero element, the diagonal of the zero matrix of size $n \times n$ over $\alpha$ is equal to the zero function, i.e., $\text{diag}(0) = 0$.
Matrix.diag_add theorem
[Add α] (A B : Matrix n n α) : diag (A + B) = diag A + diag B
Full source 
@[simp]
theorem diag_add [Add α] (A B : Matrix n n α) : diag (A + B) = diag A + diag B :=
  rfl
Diagonal of Matrix Sum Equals Sum of Diagonals
Informal description
For any type $\alpha$ with an addition operation and any two square matrices $A, B$ of size $n \times n$ over $\alpha$, the diagonal of their sum is equal to the sum of their diagonals, i.e., $\text{diag}(A + B) = \text{diag}(A) + \text{diag}(B)$.
Matrix.diag_sub theorem
[Sub α] (A B : Matrix n n α) : diag (A - B) = diag A - diag B
Full source 
@[simp]
theorem diag_sub [Sub α] (A B : Matrix n n α) : diag (A - B) = diag A - diag B :=
  rfl
Diagonal of Matrix Difference Equals Difference of Diagonals
Informal description
For any type $\alpha$ with a subtraction operation and any two square matrices $A, B$ of size $n \times n$ over $\alpha$, the diagonal of their difference is equal to the difference of their diagonals, i.e., $\text{diag}(A - B) = \text{diag}(A) - \text{diag}(B)$.
Matrix.diag_neg theorem
[Neg α] (A : Matrix n n α) : diag (-A) = -diag A
Full source 
@[simp]
theorem diag_neg [Neg α] (A : Matrix n n α) : diag (-A) = -diag A :=
  rfl
Diagonal of Negated Matrix Equals Negated Diagonal
Informal description
For any type $\alpha$ with a negation operation and any square matrix $A$ of size $n \times n$ over $\alpha$, the diagonal of the negation of $A$ is equal to the negation of the diagonal of $A$, i.e., $\text{diag}(-A) = -\text{diag}(A)$.
Matrix.diag_smul theorem
[SMul R α] (r : R) (A : Matrix n n α) : diag (r • A) = r • diag A
Full source 
@[simp]
theorem diag_smul [SMul R α] (r : R) (A : Matrix n n α) : diag (r • A) = r • diag A :=
  rfl
Diagonal of Scalar Multiple of Matrix Equals Scalar Multiple of Diagonal
Informal description
For any scalar $r$ in a type $R$ with a scalar multiplication operation on $\alpha$, and for any square matrix $A$ of size $n \times n$ over $\alpha$, the diagonal of the scalar multiple $r \cdot A$ is equal to the scalar multiple $r$ applied to the diagonal of $A$, i.e., $\text{diag}(r \cdot A) = r \cdot \text{diag}(A)$.
Matrix.diag_one theorem
[DecidableEq n] [Zero α] [One α] : diag (1 : Matrix n n α) = 1
Full source 
@[simp]
theorem diag_one [DecidableEq n] [Zero α] [One α] : diag (1 : Matrix n n α) = 1 :=
  diag_diagonal _
Diagonal of Identity Matrix Equals Constant One Function
Informal description
For any type `n` with decidable equality and any type `α` with zero and one elements, the diagonal of the identity matrix of size $n \times n$ over $\alpha$ is equal to the constant function $1 : n \to \alpha$. That is, $\text{diag}(I) = 1$, where $I$ is the identity matrix and $1$ denotes the function that maps every index to the multiplicative identity in $\alpha$.
Matrix.diag_map theorem
{f : α → β} {A : Matrix n n α} : diag (A.map f) = f ∘ diag A
Full source 
theorem diag_map {f : α → β} {A : Matrix n n α} : diag (A.map f) = f ∘ diag A :=
  rfl
Diagonal Preservation Under Matrix Mapping
Informal description
For any function $f : \alpha \to \beta$ and any square matrix $A$ of size $n \times n$ with entries in $\alpha$, the diagonal of the matrix obtained by applying $f$ to each entry of $A$ is equal to the composition of $f$ with the diagonal of $A$. In other words, $\text{diag}(A.map(f)) = f \circ \text{diag}(A)$.
Matrix.transpose_eq_diagonal theorem
[DecidableEq n] [Zero α] {M : Matrix n n α} {v : n → α} : Mᵀ = diagonal v ↔ M = diagonal v
Full source 
@[simp]
theorem transpose_eq_diagonal [DecidableEq n] [Zero α] {M : Matrix n n α} {v : n → α} :
    MᵀMᵀ = diagonal v ↔ M = diagonal v :=
  (Function.Involutive.eq_iff transpose_transpose).trans <|
    by rw [diagonal_transpose]
Transpose Equals Diagonal Matrix if and only if Matrix is Diagonal
Informal description
For a square matrix $M$ of size $n \times n$ over a type $\alpha$ with a zero element and decidable equality on $n$, the transpose of $M$ equals a diagonal matrix constructed from a vector $v : n \to \alpha$ if and only if $M$ itself equals that diagonal matrix. In other words, $M^\top = \text{diagonal } v$ if and only if $M = \text{diagonal } v$.
Matrix.transpose_one theorem
[DecidableEq n] [Zero α] [One α] : (1 : Matrix n n α)ᵀ = 1
Full source 
@[simp]
theorem transpose_one [DecidableEq n] [Zero α] [One α] : (1 : Matrix n n α)ᵀ = 1 :=
  diagonal_transpose _
Transpose of Identity Matrix is Identity
Informal description
For any type `n` with decidable equality and any type `α` with zero and one elements, the transpose of the identity matrix of size `n × n` over `α` is equal to the identity matrix itself. That is, $(1 : \text{Matrix } n n \alpha)^\top = 1$.
Matrix.transpose_eq_one theorem
[DecidableEq n] [Zero α] [One α] {M : Matrix n n α} : Mᵀ = 1 ↔ M = 1
Full source 
@[simp]
theorem transpose_eq_one [DecidableEq n] [Zero α] [One α] {M : Matrix n n α} : MᵀMᵀ = 1 ↔ M = 1 :=
  transpose_eq_diagonal
Transpose Equals Identity Matrix if and only if Matrix is Identity
Informal description
For a square matrix $M$ of size $n \times n$ over a type $\alpha$ with zero and one elements and decidable equality on $n$, the transpose of $M$ equals the identity matrix if and only if $M$ itself equals the identity matrix. That is, $M^\top = 1$ if and only if $M = 1$.
Matrix.transpose_natCast theorem
[DecidableEq n] [AddMonoidWithOne α] (d : ℕ) : (d : Matrix n n α)ᵀ = d
Full source 
@[simp]
theorem transpose_natCast [DecidableEq n] [AddMonoidWithOne α] (d : ℕ) :
    (d : Matrix n n α)ᵀ = d :=
  diagonal_transpose _
Transpose of Natural Number Cast as Diagonal Matrix
Informal description
For any type `n` with decidable equality and any type `α` with an additive monoid structure with one, the transpose of the natural number `d` cast as a diagonal matrix (with `d` on the diagonal and zeros elsewhere) is equal to the matrix itself. That is, $(d : \text{Matrix } n n \alpha)^\top = d$.
Matrix.transpose_eq_natCast theorem
[DecidableEq n] [AddMonoidWithOne α] {M : Matrix n n α} {d : ℕ} : Mᵀ = d ↔ M = d
Full source 
@[simp]
theorem transpose_eq_natCast [DecidableEq n] [AddMonoidWithOne α] {M : Matrix n n α} {d : ℕ} :
    MᵀMᵀ = d ↔ M = d :=
  transpose_eq_diagonal
Transpose Equals Natural Number Cast if and only if Matrix Equals Natural Number Cast
Informal description
For a square matrix $M$ of size $n \times n$ over a type $\alpha$ with an additive monoid structure with one and decidable equality on $n$, the transpose of $M$ equals the natural number $d$ cast as a diagonal matrix if and only if $M$ itself equals $d$ cast as a diagonal matrix. In other words, $M^\top = d$ if and only if $M = d$.
Matrix.transpose_ofNat theorem
[DecidableEq n] [AddMonoidWithOne α] (d : ℕ) [d.AtLeastTwo] : (ofNat(d) : Matrix n n α)ᵀ = OfNat.ofNat d
Full source 
@[simp]
theorem transpose_ofNat [DecidableEq n] [AddMonoidWithOne α] (d : ℕ) [d.AtLeastTwo] :
    (ofNat(d) : Matrix n n α)ᵀ = OfNat.ofNat d :=
  transpose_natCast _
Transpose of Diagonal Matrix from Natural Number at Least Two Equals Itself
Informal description
For any type `n` with decidable equality and any type `α` with an additive monoid structure with one, and for any natural number `d` that is at least two, the transpose of the diagonal matrix with `d` (as an element of `α`) on every diagonal entry and zero elsewhere is equal to the matrix itself. That is, $(d : \text{Matrix } n n \alpha)^\top = d$.
Matrix.transpose_eq_ofNat theorem
[DecidableEq n] [AddMonoidWithOne α] {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] : Mᵀ = ofNat(d) ↔ M = OfNat.ofNat d
Full source 
@[simp]
theorem transpose_eq_ofNat [DecidableEq n] [AddMonoidWithOne α]
    {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] :
    MᵀMᵀ = ofNat(d) ↔ M = OfNat.ofNat d :=
  transpose_eq_diagonal
Transpose Equals Scalar Matrix $d \cdot I_n$ if and only if Matrix is $d \cdot I_n$ for $d \geq 2$
Informal description
For a square matrix $M$ of size $n \times n$ over a type $\alpha$ with an additive monoid structure with one and decidable equality on $n$, and for a natural number $d \geq 2$, the transpose of $M$ equals the scalar matrix $d \cdot I_n$ if and only if $M$ itself equals $d \cdot I_n$. In other words, $M^\top = d \cdot I_n$ if and only if $M = d \cdot I_n$.
Matrix.transpose_intCast theorem
[DecidableEq n] [AddGroupWithOne α] (d : ℤ) : (d : Matrix n n α)ᵀ = d
Full source 
@[simp]
theorem transpose_intCast [DecidableEq n] [AddGroupWithOne α] (d : ℤ) :
    (d : Matrix n n α)ᵀ = d :=
  diagonal_transpose _
Transpose of Integer Scalar Matrix Equals Itself
Informal description
For any type `n` with decidable equality and any type `α` with an additive group structure with one, the transpose of the scalar matrix $d \cdot I_n$ (where $d \in \mathbb{Z}$ and $I_n$ is the identity matrix) is equal to itself, i.e., $(d \cdot I_n)^\top = d \cdot I_n$.
Matrix.transpose_eq_intCast theorem
[DecidableEq n] [AddGroupWithOne α] {M : Matrix n n α} {d : ℤ} : Mᵀ = d ↔ M = d
Full source 
@[simp]
theorem transpose_eq_intCast [DecidableEq n] [AddGroupWithOne α]
    {M : Matrix n n α} {d : ℤ} :
    MᵀMᵀ = d ↔ M = d :=
  transpose_eq_diagonal
Transpose Equals Integer Scalar Matrix if and only if Matrix is Scalar Matrix
Informal description
For a square matrix $M$ of size $n \times n$ over a type $\alpha$ with an additive group structure with one and decidable equality on $n$, the transpose of $M$ equals the integer scalar matrix $d \cdot I_n$ if and only if $M$ itself equals $d \cdot I_n$. That is, \[ M^\top = d \cdot I_n \leftrightarrow M = d \cdot I_n. \]
Matrix.submatrix_diagonal theorem
[Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l → m) (he : Function.Injective e) : (diagonal d).submatrix e e = diagonal (d ∘ e)
Full source 
/-- Given a `(m × m)` diagonal matrix defined by a map `d : m → α`, if the reindexing map `e` is
  injective, then the resulting matrix is again diagonal. -/
theorem submatrix_diagonal [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l → m)
    (he : Function.Injective e) : (diagonal d).submatrix e e = diagonal (d ∘ e) :=
  ext fun i j => by
    rw [submatrix_apply]
    by_cases h : i = j
    · rw [h, diagonal_apply_eq, diagonal_apply_eq, Function.comp_apply]
    · rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]
Submatrix of Diagonal Matrix Preserves Diagonal Structure under Injective Reindexing
Informal description
Let $m$ and $l$ be types with decidable equality, and let $\alpha$ be a type with a zero element. Given a vector $d : m \to \alpha$ and an injective function $e : l \to m$, the submatrix of the diagonal matrix $\text{diagonal}(d)$ obtained by selecting rows and columns according to $e$ is equal to the diagonal matrix constructed from the composition $d \circ e$. That is, \[ (\text{diagonal } d).\text{submatrix}\ e\ e = \text{diagonal}(d \circ e). \]
Matrix.submatrix_one theorem
[Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l → m) (he : Function.Injective e) : (1 : Matrix m m α).submatrix e e = 1
Full source 
theorem submatrix_one [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l → m)
    (he : Function.Injective e) : (1 : Matrix m m α).submatrix e e = 1 :=
  submatrix_diagonal _ e he
Submatrix of Identity Matrix under Injective Reindexing is Identity Matrix
Informal description
Let $m$ and $l$ be types with decidable equality, and let $\alpha$ be a type with zero and one elements. For any injective function $e : l \to m$, the submatrix of the identity matrix (of size $m \times m$) obtained by selecting rows and columns according to $e$ is equal to the identity matrix (of size $l \times l$). That is, \[ (1 : \text{Matrix}\ m\ m\ \alpha).\text{submatrix}\ e\ e = 1. \]
Matrix.diag_submatrix theorem
(A : Matrix m m α) (e : l → m) : diag (A.submatrix e e) = A.diag ∘ e
Full source 
theorem diag_submatrix (A : Matrix m m α) (e : l → m) : diag (A.submatrix e e) = A.diag ∘ e :=
  rfl
Diagonal of Submatrix Equals Composition of Diagonal with Index Function
Informal description
For any square matrix $A$ of size $m \times m$ over a type $\alpha$ and any function $e : l \to m$, the diagonal of the submatrix of $A$ obtained by selecting rows and columns according to $e$ is equal to the composition of the diagonal of $A$ with $e$, i.e., $\text{diag}(A.\text{submatrix}\ e\ e) = \text{diag}(A) \circ e$.
Matrix.submatrix_diagonal_embedding theorem
[Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l ↪ m) : (diagonal d).submatrix e e = diagonal (d ∘ e)
Full source 
@[simp]
theorem submatrix_diagonal_embedding [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α)
    (e : l ↪ m) : (diagonal d).submatrix e e = diagonal (d ∘ e) :=
  submatrix_diagonal d e e.injective
Submatrix of Diagonal Matrix under Embedding Preserves Diagonal Structure
Informal description
Let $\alpha$ be a type with a zero element, and let $m$ and $l$ be types with decidable equality. Given a vector $d : m \to \alpha$ and an embedding $e : l \hookrightarrow m$, the submatrix of the diagonal matrix $\text{diag}(d)$ obtained by selecting rows and columns according to $e$ is equal to the diagonal matrix constructed from the composition $d \circ e$. That is, \[ (\text{diag}(d)).\text{submatrix}\ e\ e = \text{diag}(d \circ e). \]
Matrix.submatrix_diagonal_equiv theorem
[Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l ≃ m) : (diagonal d).submatrix e e = diagonal (d ∘ e)
Full source 
@[simp]
theorem submatrix_diagonal_equiv [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l ≃ m) :
    (diagonal d).submatrix e e = diagonal (d ∘ e) :=
  submatrix_diagonal d e e.injective
Submatrix of Diagonal Matrix under Equivalence Preserves Diagonal Structure
Informal description
Let $m$ and $l$ be types with decidable equality, and let $\alpha$ be a type with a zero element. Given a vector $d : m \to \alpha$ and an equivalence $e : l \simeq m$, the submatrix of the diagonal matrix $\text{diagonal}(d)$ obtained by selecting rows and columns according to $e$ is equal to the diagonal matrix constructed from the composition $d \circ e$. That is, \[ (\text{diagonal } d).\text{submatrix}\ e\ e = \text{diagonal}(d \circ e). \]
Matrix.submatrix_one_embedding theorem
[Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l ↪ m) : (1 : Matrix m m α).submatrix e e = 1
Full source 
@[simp]
theorem submatrix_one_embedding [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l ↪ m) :
    (1 : Matrix m m α).submatrix e e = 1 :=
  submatrix_one e e.injective
Identity Submatrix Preservation under Embedding
Informal description
Let $m$ and $l$ be types with decidable equality, and let $\alpha$ be a type with zero and one elements. For any embedding $e : l \hookrightarrow m$, the submatrix of the identity matrix (of size $m \times m$) obtained by selecting rows and columns according to $e$ is equal to the identity matrix (of size $l \times l$). That is, \[ (1 : \text{Matrix}\ m\ m\ \alpha).\text{submatrix}\ e\ e = 1. \]
Matrix.submatrix_one_equiv theorem
[Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l ≃ m) : (1 : Matrix m m α).submatrix e e = 1
Full source 
@[simp]
theorem submatrix_one_equiv [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l ≃ m) :
    (1 : Matrix m m α).submatrix e e = 1 :=
  submatrix_one e e.injective
Identity Matrix Submatrix Preservation under Equivalence
Informal description
Let $m$ and $l$ be types with decidable equality, and let $\alpha$ be a type with zero and one elements. For any equivalence $e : l \simeq m$, the submatrix of the identity matrix (of size $m \times m$) obtained by selecting rows and columns according to $e$ is equal to the identity matrix (of size $l \times l$). That is, \[ (1 : \text{Matrix}\ m\ m\ \alpha).\text{submatrix}\ e\ e = 1. \]