Mathlib.LinearAlgebra.Matrix.Trace

Matrix.trace definition

(A : Matrix n n R) : R

Full source

/-- The trace of a square matrix. For more bundled versions, see:
* `Matrix.traceAddMonoidHom`
* `Matrix.traceLinearMap`
-/
def trace (A : Matrix n n R) : R :=
  ∑ i, diag A i

Trace of a square matrix

Informal description

The trace of a square matrix $A$ over a ring $R$ is the sum of its diagonal elements, i.e., $\text{trace}(A) = \sum_i A_{i,i}$.

Matrix.trace_diagonal theorem

{o} [Fintype o] [DecidableEq o] (d : o → R) : trace (diagonal d) = ∑ i, d i

Full source

lemma trace_diagonal {o} [Fintype o] [DecidableEq o] (d : o → R) :
    trace (diagonal d) = ∑ i, d i := by
  simp only [trace, diag_apply, diagonal_apply_eq]

Trace of Diagonal Matrix Equals Sum of Diagonal Entries

Informal description

For any finite type $o$ with decidable equality and any vector $d : o \to R$ over a ring $R$, the trace of the diagonal matrix constructed from $d$ is equal to the sum of the elements of $d$, i.e., \[ \text{trace}(\text{diagonal } d) = \sum_{i} d_i. \]

Matrix.trace_zero theorem

: trace (0 : Matrix n n R) = 0

Full source

@[simp]
theorem trace_zero : trace (0 : Matrix n n R) = 0 :=
  (Finset.sum_const (0 : R)).trans <| smul_zero _

Trace of Zero Matrix is Zero

Informal description

The trace of the zero matrix of size $n \times n$ over a ring $R$ is equal to zero, i.e., $\text{trace}(0) = 0$.

Matrix.trace_eq_zero_of_isEmpty theorem

[IsEmpty n] (A : Matrix n n R) : trace A = 0

Full source

@[simp]
lemma trace_eq_zero_of_isEmpty [IsEmpty n] (A : Matrix n n R) : trace A = 0 := by simp [trace]

Trace of Matrix over Empty Index Type is Zero

Informal description

For any square matrix $A$ of size $n \times n$ over a ring $R$, if the index type $n$ is empty, then the trace of $A$ is zero, i.e., $\text{trace}(A) = 0$.

Matrix.trace_add theorem

(A B : Matrix n n R) : trace (A + B) = trace A + trace B

Full source

@[simp]
theorem trace_add (A B : Matrix n n R) : trace (A + B) = trace A + trace B :=
  Finset.sum_add_distrib

Additivity of Matrix Trace: $\text{trace}(A + B) = \text{trace}(A) + \text{trace}(B)$

Informal description

For any two square matrices $A$ and $B$ of size $n \times n$ over a ring $R$, the trace of their sum equals the sum of their traces, i.e., $\text{trace}(A + B) = \text{trace}(A) + \text{trace}(B)$.

Matrix.trace_smul theorem

[DistribSMul α R] (r : α) (A : Matrix n n R) : trace (r • A) = r • trace A

Full source

@[simp]
theorem trace_smul [DistribSMul α R] (r : α) (A : Matrix n n R) :
    trace (r • A) = r • trace A :=
  Finset.smul_sum.symm

Trace of Scalar Multiple Equals Scalar Multiple of Trace

Informal description

For any scalar $r$ in a type $\alpha$ with a distributive scalar multiplication structure over a ring $R$, and for any square matrix $A$ of size $n \times n$ with entries in $R$, the trace of the scalar multiple $r \cdot A$ is equal to the scalar multiple of the trace of $A$, i.e., $\text{trace}(r \cdot A) = r \cdot \text{trace}(A)$.

Matrix.trace_transpose theorem

(A : Matrix n n R) : trace Aᵀ = trace A

Full source

@[simp]
theorem trace_transpose (A : Matrix n n R) : trace Aᵀ = trace A :=
  rfl

Trace Invariance Under Transposition: $\text{trace}(A^\top) = \text{trace}(A)$

Informal description

For any square matrix $A$ of size $n \times n$ with entries in a ring $R$, the trace of the transpose of $A$ is equal to the trace of $A$, i.e., $\text{trace}(A^\top) = \text{trace}(A)$.

Matrix.trace_conjTranspose theorem

[StarAddMonoid R] (A : Matrix n n R) : trace Aᴴ = star (trace A)

Full source

@[simp]
theorem trace_conjTranspose [StarAddMonoid R] (A : Matrix n n R) : trace Aᴴ = star (trace A) :=
  (star_sum _ _).symm

Trace of Conjugate Transpose Equals Star of Trace

Informal description

For any square matrix $A$ of size $n \times n$ with entries in a ring $R$ equipped with a star operation and an additive monoid structure, the trace of the conjugate transpose of $A$ equals the star of the trace of $A$, i.e., $\text{trace}(A^H) = \text{star}(\text{trace}(A))$.

Matrix.traceAddMonoidHom definition

: Matrix n n R →+ R

Full source

/-- `Matrix.trace` as an `AddMonoidHom` -/
@[simps]
def traceAddMonoidHom : MatrixMatrix n n R →+ R where
  toFun := trace
  map_zero' := trace_zero n R
  map_add' := trace_add

Trace as an additive monoid homomorphism

Informal description

The additive monoid homomorphism version of the matrix trace function, which sends a square matrix $A$ of size $n \times n$ over a ring $R$ to the sum of its diagonal elements, $\sum_i A_{i,i}$. This map preserves addition and the zero matrix, satisfying: 1. $\text{trace}(0) = 0$ 2. $\text{trace}(A + B) = \text{trace}(A) + \text{trace}(B)$ for any matrices $A, B$

Matrix.traceLinearMap definition

[Semiring α] [Module α R] : Matrix n n R →ₗ[α] R

Full source

/-- `Matrix.trace` as a `LinearMap` -/
@[simps]
def traceLinearMap [Semiring α] [Module α R] : MatrixMatrix n n R →ₗ[α] R where
  toFun := trace
  map_add' := trace_add
  map_smul' := trace_smul

Linear map of matrix trace

Informal description

The linear map version of the matrix trace function, which sends a square matrix $A$ of size $n \times n$ over a ring $R$ (with $R$ being a module over a semiring $\alpha$) to the sum of its diagonal elements, $\sum_i A_{i,i}$. This map is linear, meaning it preserves addition and scalar multiplication.

Matrix.trace_list_sum theorem

(l : List (Matrix n n R)) : trace l.sum = (l.map trace).sum

Full source

@[simp]
theorem trace_list_sum (l : List (Matrix n n R)) : trace l.sum = (l.map trace).sum :=
  map_list_sum (traceAddMonoidHom n R) l

Trace of Sum of Matrices Equals Sum of Traces for Lists

Informal description

For any list $l$ of square matrices over a ring $R$, the trace of the sum of the matrices in $l$ is equal to the sum of the traces of the matrices in $l$. That is, \[ \text{trace}\left(\sum_{A \in l} A\right) = \sum_{A \in l} \text{trace}(A). \]

Matrix.trace_multiset_sum theorem

(s : Multiset (Matrix n n R)) : trace s.sum = (s.map trace).sum

Full source

@[simp]
theorem trace_multiset_sum (s : Multiset (Matrix n n R)) : trace s.sum = (s.map trace).sum :=
  map_multiset_sum (traceAddMonoidHom n R) s

Trace of Sum of Multiset of Matrices Equals Sum of Traces

Informal description

For any multiset $s$ of $n \times n$ matrices over a ring $R$, the trace of the sum of the matrices in $s$ is equal to the sum of their traces, i.e., \[ \text{trace}\left(\sum_{A \in s} A\right) = \sum_{A \in s} \text{trace}(A). \]

Matrix.trace_sum theorem

(s : Finset ι) (f : ι → Matrix n n R) : trace (∑ i ∈ s, f i) = ∑ i ∈ s, trace (f i)

Full source

@[simp]
theorem trace_sum (s : Finset ι) (f : ι → Matrix n n R) :
    trace (∑ i ∈ s, f i) = ∑ i ∈ s, trace (f i) :=
  map_sum (traceAddMonoidHom n R) f s

Trace of Sum Equals Sum of Traces for Finite Families of Matrices

Informal description

For any finite set $s$ and any family of square matrices $f : \iota \to \text{Matrix}_n(R)$, the trace of the sum of the matrices equals the sum of their traces: \[ \text{trace}\left(\sum_{i \in s} f(i)\right) = \sum_{i \in s} \text{trace}(f(i)). \]

AddMonoidHom.map_trace theorem

 [AddCommMonoid S] {F : Type*} [FunLike F R S] [AddMonoidHomClass F R S] (f : F) (A : Matrix n n R) :
  f (trace A) = trace ((f : R →+ S).mapMatrix A)

Full source

theorem _root_.AddMonoidHom.map_trace [AddCommMonoid S] {F : Type*} [FunLike F R S]
    [AddMonoidHomClass F R S] (f : F) (A : Matrix n n R) :
    f (trace A) = trace ((f : R →+ S).mapMatrix A) :=
  map_sum f (fun i => diag A i) Finset.univ

Additive Monoid Homomorphism Preserves Trace of Matrix

Informal description

Let $R$ and $S$ be additive commutative monoids, and let $F$ be a type of functions from $R$ to $S$ that preserves the additive structure (i.e., $F$ is an `AddMonoidHomClass`). For any additive monoid homomorphism $f \colon R \to S$ and any square matrix $A$ over $R$, the image of the trace of $A$ under $f$ equals the trace of the matrix obtained by applying $f$ to each entry of $A$, i.e., \[ f(\text{trace}(A)) = \text{trace}(f_{\text{matrix}}(A)), \] where $f_{\text{matrix}}(A)$ denotes the matrix obtained by applying $f$ to each entry of $A$.

Matrix.trace_blockDiagonal theorem

[DecidableEq p] (M : p → Matrix n n R) : trace (blockDiagonal M) = ∑ i, trace (M i)

Full source

lemma trace_blockDiagonal [DecidableEq p] (M : p → Matrix n n R) :
    trace (blockDiagonal M) = ∑ i, trace (M i) := by
  simp [blockDiagonal, trace, Finset.sum_comm (γ := n), Fintype.sum_prod_type]

Trace of Block-Diagonal Matrix Equals Sum of Traces of Blocks

Informal description

For a family of square matrices $M_i$ over a ring $R$, where each $M_i$ has size $n \times n$, the trace of the block-diagonal matrix formed by placing each $M_i$ along the diagonal is equal to the sum of the traces of the individual matrices $M_i$, i.e., $\text{trace}(\text{blockDiagonal } M) = \sum_i \text{trace}(M_i)$.

Matrix.trace_blockDiagonal' theorem

 [DecidableEq p] {m : p → Type*} [∀ i, Fintype (m i)] (M : ∀ i, Matrix (m i) (m i) R) :
  trace (blockDiagonal' M) = ∑ i, trace (M i)

Full source

lemma trace_blockDiagonal' [DecidableEq p] {m : p → Type*} [∀ i, Fintype (m i)]
    (M : ∀ i, Matrix (m i) (m i) R) :
    trace (blockDiagonal' M) = ∑ i, trace (M i) := by
  simp [blockDiagonal', trace, Finset.sum_sigma']

Trace of Block-Diagonal Matrix Equals Sum of Traces of Blocks

Informal description

For a family of square matrices $M_i$ over a ring $R$, where each $M_i$ has size $m_i \times m_i$ and $m_i$ is finite for each $i$, the trace of the block-diagonal matrix formed by placing each $M_i$ along the diagonal is equal to the sum of the traces of the individual matrices $M_i$, i.e., $\text{trace}(\text{blockDiagonal}' M) = \sum_i \text{trace}(M_i)$.

Matrix.trace_sub theorem

(A B : Matrix n n R) : trace (A - B) = trace A - trace B

Full source

@[simp]
theorem trace_sub (A B : Matrix n n R) : trace (A - B) = trace A - trace B :=
  Finset.sum_sub_distrib

Trace of Matrix Difference Equals Difference of Traces

Informal description

For any two square matrices $A$ and $B$ of size $n \times n$ over a ring $R$, the trace of their difference equals the difference of their traces, i.e., $\text{trace}(A - B) = \text{trace}(A) - \text{trace}(B)$.

Matrix.trace_neg theorem

(A : Matrix n n R) : trace (-A) = -trace A

Full source

@[simp]
theorem trace_neg (A : Matrix n n R) : trace (-A) = -trace A :=
  Finset.sum_neg_distrib

Trace of Negated Matrix Equals Negation of Trace: $\text{trace}(-A) = -\text{trace}(A)$

Informal description

For any square matrix $A$ of size $n \times n$ over a ring $R$, the trace of $-A$ equals the negation of the trace of $A$, i.e., $\text{trace}(-A) = -\text{trace}(A)$.

Matrix.trace_one theorem

: trace (1 : Matrix n n R) = Fintype.card n

Full source

@[simp]
theorem trace_one : trace (1 : Matrix n n R) = Fintype.card n := by
  simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]

Trace of Identity Matrix Equals Cardinality of Index Set

Informal description

For any finite type `n` and any ring `R`, the trace of the identity matrix of size $n \times n$ over `R` is equal to the cardinality of `n$, i.e., $\text{trace}(I_n) = |n|$.

Matrix.trace_transpose_mul theorem

[AddCommMonoid R] [Mul R] (A : Matrix m n R) (B : Matrix n m R) : trace (Aᵀ * Bᵀ) = trace (A * B)

Full source

@[simp]
theorem trace_transpose_mul [AddCommMonoid R] [Mul R] (A : Matrix m n R) (B : Matrix n m R) :
    trace (Aᵀ * Bᵀ) = trace (A * B) :=
  Finset.sum_comm

Trace Identity for Transposed Matrix Multiplication

Informal description

Let $R$ be an additive commutative monoid with a multiplication operation, and let $A$ be an $m \times n$ matrix and $B$ an $n \times m$ matrix over $R$. Then the trace of the product of the transpose of $A$ with the transpose of $B$ equals the trace of the product $AB$, i.e., \[ \text{trace}(A^\top B^\top) = \text{trace}(AB). \]

Matrix.trace_mul_comm theorem

[AddCommMonoid R] [CommMagma R] (A : Matrix m n R) (B : Matrix n m R) : trace (A * B) = trace (B * A)

Full source

theorem trace_mul_comm [AddCommMonoid R] [CommMagma R] (A : Matrix m n R) (B : Matrix n m R) :
    trace (A * B) = trace (B * A) := by rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]

Trace Commutativity: $\text{trace}(AB) = \text{trace}(BA)$

Informal description

Let $R$ be an additive commutative monoid with a commutative multiplication operation, and let $A$ be an $m \times n$ matrix and $B$ an $n \times m$ matrix over $R$. Then the trace of the product $AB$ equals the trace of the product $BA$, i.e., \[ \text{trace}(AB) = \text{trace}(BA). \]

Matrix.trace_mul_cycle theorem

 [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R) :
  trace (A * B * C) = trace (C * A * B)

Full source

theorem trace_mul_cycle [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R)
    (C : Matrix p m R) : trace (A * B * C) = trace (C * A * B) := by
  rw [trace_mul_comm, Matrix.mul_assoc]

Trace Cyclic Permutation Identity: $\text{trace}(ABC) = \text{trace}(CAB)$

Informal description

Let $R$ be a non-unital commutative semiring, and let $A$ be an $m \times n$ matrix, $B$ an $n \times p$ matrix, and $C$ a $p \times m$ matrix over $R$. Then the trace of the product $ABC$ equals the trace of the product $CAB$, i.e., \[ \text{trace}(ABC) = \text{trace}(CAB). \]

Matrix.trace_mul_cycle' theorem

 [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R) :
  trace (A * (B * C)) = trace (C * (A * B))

Full source

theorem trace_mul_cycle' [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R)
    (C : Matrix p m R) : trace (A * (B * C)) = trace (C * (A * B)) := by
  rw [← Matrix.mul_assoc, trace_mul_comm]

Trace Cyclic Permutation Identity: $\text{trace}(A(BC)) = \text{trace}(C(AB))$

Informal description

Let $R$ be a non-unital commutative semiring, and let $A$ be an $m \times n$ matrix, $B$ an $n \times p$ matrix, and $C$ a $p \times m$ matrix over $R$. Then the trace of the product $A(BC)$ equals the trace of the product $C(AB)$, i.e., \[ \text{trace}(A(BC)) = \text{trace}(C(AB)). \]

Matrix.trace_replicateCol_mul_replicateRow theorem

 {ι : Type*} [Unique ι] [NonUnitalNonAssocSemiring R] (a b : n → R) :
  trace (replicateCol ι a * replicateRow ι b) = dotProduct a b

Full source

@[simp]
theorem trace_replicateCol_mul_replicateRow {ι : Type*} [Unique ι] [NonUnitalNonAssocSemiring R]
    (a b : n → R) : trace (replicateCol ι a * replicateRow ι b) = dotProduct a b := by
  apply Finset.sum_congr rfl
  simp [mul_apply]

Trace of Product of Replicated Column and Row Matrices Equals Dot Product

Informal description

Let $R$ be a non-unital non-associative semiring, and let $\iota$ be a type with a unique element. For any vectors $a, b : n \to R$, the trace of the product of the matrix with replicated columns $a$ and the matrix with replicated rows $b$ equals the dot product of $a$ and $b$, i.e., \[ \text{trace}(\text{replicateCol}_\iota a \cdot \text{replicateRow}_\iota b) = a \cdot b. \]

Matrix.trace_submatrix_succ theorem

 {n : ℕ} [AddCommMonoid R] (M : Matrix (Fin n.succ) (Fin n.succ) R) :
  M 0 0 + trace (submatrix M Fin.succ Fin.succ) = trace M

Full source

lemma trace_submatrix_succ {n : ℕ} [AddCommMonoid R]
    (M : Matrix (Fin n.succ) (Fin n.succ) R) :
    M 0 0 + trace (submatrix M Fin.succ Fin.succ) = trace M := by
  delta trace
  rw [← (finSuccEquiv n).symm.sum_comp]
  simp

Trace Decomposition for $(n+1) \times (n+1)$ Matrices: $M_{0,0} + \text{trace}(\text{submatrix}) = \text{trace}(M)$

Informal description

For any $(n+1) \times (n+1)$ matrix $M$ over an additive commutative monoid $R$, the trace of $M$ is equal to the sum of its top-left entry $M_{0,0}$ and the trace of the submatrix obtained by removing the first row and first column, i.e., \[ M_{0,0} + \text{trace}(\text{submatrix}\,M\,\text{Fin.succ}\,\text{Fin.succ}) = \text{trace}\,M. \]

Matrix.trace_units_conj theorem

(M : (Matrix m m R)ˣ) (N : Matrix m m R) : trace ((M : Matrix _ _ _) * N * (↑M⁻¹ : Matrix _ _ _)) = trace N

Full source

theorem trace_units_conj (M : (Matrix m m R)ˣ) (N : Matrix m m R) :
    trace ((M : Matrix _ _ _) * N * (↑M⁻¹ : Matrix _ _ _)) = trace N := by
  rw [trace_mul_cycle, Units.inv_mul, one_mul]

Trace Invariance Under Matrix Conjugation: $\text{trace}(M N M^{-1}) = \text{trace}(N)$

Informal description

Let $R$ be a ring and let $M$ be an invertible $m \times m$ matrix over $R$. For any $m \times m$ matrix $N$ over $R$, the trace of $M N M^{-1}$ equals the trace of $N$, i.e., \[ \text{trace}(M N M^{-1}) = \text{trace}(N). \]

Matrix.trace_units_conj' theorem

(M : (Matrix m m R)ˣ) (N : Matrix m m R) : trace ((↑M⁻¹ : Matrix _ _ _) * N * (↑M : Matrix _ _ _)) = trace N

Full source

theorem trace_units_conj' (M : (Matrix m m R)ˣ) (N : Matrix m m R) :
    trace ((↑M⁻¹ : Matrix _ _ _) * N * (↑M : Matrix _ _ _)) = trace N :=
  trace_units_conj M⁻¹ N

Trace Invariance Under Matrix Conjugation: $\text{trace}(M^{-1} N M) = \text{trace}(N)$

Informal description

Let $R$ be a ring and let $M$ be an invertible $m \times m$ matrix over $R$. For any $m \times m$ matrix $N$ over $R$, the trace of $M^{-1} N M$ equals the trace of $N$, i.e., \[ \text{trace}(M^{-1} N M) = \text{trace}(N). \]

Matrix.trace_fin_zero theorem

(A : Matrix (Fin 0) (Fin 0) R) : trace A = 0

Full source

@[simp]
theorem trace_fin_zero (A : Matrix (Fin 0) (Fin 0) R) : trace A = 0 :=
  rfl

Trace of a $0 \times 0$ Matrix is Zero

Informal description

For any matrix $A$ of size $0 \times 0$ over a ring $R$, the trace of $A$ is equal to $0$.

Matrix.trace_fin_one theorem

(A : Matrix (Fin 1) (Fin 1) R) : trace A = A 0 0

Full source

theorem trace_fin_one (A : Matrix (Fin 1) (Fin 1) R) : trace A = A 0 0 :=
  add_zero _

Trace of a $1 \times 1$ matrix equals its single entry

Informal description

For any $1 \times 1$ matrix $A$ over a ring $R$, the trace of $A$ is equal to its single diagonal entry, i.e., $\text{trace}(A) = A_{0,0}$.

Matrix.trace_fin_two theorem

(A : Matrix (Fin 2) (Fin 2) R) : trace A = A 0 0 + A 1 1

Full source

theorem trace_fin_two (A : Matrix (Fin 2) (Fin 2) R) : trace A = A 0 0 + A 1 1 :=
  congr_arg (_ + ·) (add_zero (A 1 1))

Trace of a $2 \times 2$ matrix equals sum of diagonal entries

Informal description

For any $2 \times 2$ matrix $A$ over a ring $R$, the trace of $A$ is equal to the sum of its diagonal entries, i.e., $\text{trace}(A) = A_{0,0} + A_{1,1}$.

Matrix.trace_fin_three theorem

(A : Matrix (Fin 3) (Fin 3) R) : trace A = A 0 0 + A 1 1 + A 2 2

Full source

theorem trace_fin_three (A : Matrix (Fin 3) (Fin 3) R) : trace A = A 0 0 + A 1 1 + A 2 2 := by
  rw [← add_zero (A 2 2), add_assoc]
  rfl

Trace of a $3 \times 3$ matrix equals sum of diagonal entries

Informal description

For any $3 \times 3$ matrix $A$ over a ring $R$, the trace of $A$ is equal to the sum of its diagonal entries, i.e., $\text{trace}(A) = A_{0,0} + A_{1,1} + A_{2,2}$.

Matrix.trace_fin_one_of theorem

(a : R) : trace !![a] = a

Full source

@[simp]
theorem trace_fin_one_of (a : R) : trace !![a] = a :=
  trace_fin_one _

Trace of a $1 \times 1$ matrix equals its single entry

Informal description

For any element $a$ in a ring $R$, the trace of the $1 \times 1$ matrix $\begin{pmatrix}a\end{pmatrix}$ is equal to $a$.

Matrix.trace_fin_two_of theorem

(a b c d : R) : trace !![a, b; c, d] = a + d

Full source

@[simp]
theorem trace_fin_two_of (a b c d : R) : trace !![a, b; c, d] = a + d :=
  trace_fin_two _

Trace of $2 \times 2$ matrix: $\text{trace}\begin{pmatrix}a & b \\ c & d\end{pmatrix} = a + d$

Informal description

For any elements $a, b, c, d$ in a ring $R$, the trace of the $2 \times 2$ matrix $\begin{pmatrix}a & b \\ c & d\end{pmatrix}$ is equal to $a + d$.

Matrix.trace_fin_three_of theorem

(a b c d e f g h i : R) : trace !![a, b, c; d, e, f; g, h, i] = a + e + i

Full source

@[simp]
theorem trace_fin_three_of (a b c d e f g h i : R) :
    trace !![a, b, c; d, e, f; g, h, i] = a + e + i :=
  trace_fin_three _

Trace of $3 \times 3$ matrix: $\text{trace}\begin{pmatrix}a & b & c \\ d & e & f \\ g & h & i\end{pmatrix} = a + e + i$

Informal description

For any elements $a, b, c, d, e, f, g, h, i$ in a ring $R$, the trace of the $3 \times 3$ matrix $\begin{pmatrix}a & b & c \\ d & e & f \\ g & h & i\end{pmatrix}$ is equal to $a + e + i$.

Matrix.StdBasisMatrix.trace_zero theorem

(h : j ≠ i) : trace (stdBasisMatrix i j c) = 0

Full source

@[simp]
theorem trace_zero (h : j ≠ i) : trace (stdBasisMatrix i j c) = 0 := by
  -- Porting note: added `-diag_apply`
  simp [trace, -diag_apply, h]

Trace of Standard Basis Matrix with Off-Diagonal Indices is Zero

Informal description

For any indices $i$ and $j$ with $j \neq i$ and any scalar $c$, the trace of the standard basis matrix $\text{stdBasisMatrix}(i, j, c)$ is zero.

Matrix.StdBasisMatrix.trace_eq theorem

: trace (stdBasisMatrix i i c) = c

Full source

@[simp]
theorem trace_eq : trace (stdBasisMatrix i i c) = c := by
  -- Porting note: added `-diag_apply`
  simp [trace, -diag_apply]

Trace of Standard Basis Matrix with Diagonal Index Equals Scalar

Informal description

For any index $i$ and scalar $c$, the trace of the standard basis matrix $\text{stdBasisMatrix}(i, i, c)$ is equal to $c$.

Tags