Trace of a matrix #

This file defines the trace of a matrix, the map sending a matrix to the sum of its diagonal entries.

See also LinearAlgebra.Trace for the trace of an endomorphism.

Tags #

matrix, trace, diagonal

def Matrix.trace {n : Type u_3} {R : Type u_6} [] [] (A : Matrix n n R) :
R

The trace of a square matrix. For more bundled versions, see:

• Matrix.traceAddMonoidHom
• Matrix.traceLinearMap
Equations
• A.trace = i : n, A.diag i
Instances For
theorem Matrix.trace_diagonal {R : Type u_6} [] {o : Type u_8} [] [] (d : oR) :
().trace = i : o, d i
@[simp]
theorem Matrix.trace_zero (n : Type u_3) (R : Type u_6) [] [] :
@[simp]
theorem Matrix.trace_eq_zero_of_isEmpty {n : Type u_3} {R : Type u_6} [] [] [] (A : Matrix n n R) :
A.trace = 0
@[simp]
theorem Matrix.trace_add {n : Type u_3} {R : Type u_6} [] [] (A : Matrix n n R) (B : Matrix n n R) :
(A + B).trace = A.trace + B.trace
@[simp]
theorem Matrix.trace_smul {n : Type u_3} {α : Type u_5} {R : Type u_6} [] [] [] [] (r : α) (A : Matrix n n R) :
(r A).trace = r A.trace
@[simp]
theorem Matrix.trace_transpose {n : Type u_3} {R : Type u_6} [] [] (A : Matrix n n R) :
A.transpose.trace = A.trace
@[simp]
theorem Matrix.trace_conjTranspose {n : Type u_3} {R : Type u_6} [] [] [] (A : Matrix n n R) :
A.conjTranspose.trace = star A.trace
@[simp]
theorem Matrix.traceAddMonoidHom_apply (n : Type u_3) (R : Type u_6) [] [] (A : Matrix n n R) :
() A = A.trace
def Matrix.traceAddMonoidHom (n : Type u_3) (R : Type u_6) [] [] :
Matrix n n R →+ R

Matrix.trace as an AddMonoidHom

Equations
• = { toFun := Matrix.trace, map_zero' := , map_add' := }
Instances For
@[simp]
theorem Matrix.traceLinearMap_apply (n : Type u_3) (α : Type u_5) (R : Type u_6) [] [] [] [Module α R] (A : Matrix n n R) :
() A = A.trace
def Matrix.traceLinearMap (n : Type u_3) (α : Type u_5) (R : Type u_6) [] [] [] [Module α R] :
Matrix n n R →ₗ[α] R

Matrix.trace as a LinearMap

Equations
• = { toFun := Matrix.trace, map_add' := , map_smul' := }
Instances For
@[simp]
theorem Matrix.trace_list_sum {n : Type u_3} {R : Type u_6} [] [] (l : List (Matrix n n R)) :
l.sum.trace = (List.map Matrix.trace l).sum
@[simp]
theorem Matrix.trace_multiset_sum {n : Type u_3} {R : Type u_6} [] [] (s : Multiset (Matrix n n R)) :
s.sum.trace = (Multiset.map Matrix.trace s).sum
@[simp]
theorem Matrix.trace_sum {ι : Type u_1} {n : Type u_3} {R : Type u_6} [] [] (s : ) (f : ιMatrix n n R) :
(is, f i).trace = is, (f i).trace
theorem AddMonoidHom.map_trace {n : Type u_3} {R : Type u_6} {S : Type u_7} [] [] [] (f : R →+ S) (A : Matrix n n R) :
f A.trace = (f.mapMatrix A).trace
theorem Matrix.trace_blockDiagonal {n : Type u_3} {p : Type u_4} {R : Type u_6} [] [] [] [] (M : pMatrix n n R) :
.trace = i : p, (M i).trace
theorem Matrix.trace_blockDiagonal' {p : Type u_4} {R : Type u_6} [] [] [] {m : pType u_8} [(i : p) → Fintype (m i)] (M : (i : p) → Matrix (m i) (m i) R) :
.trace = i : p, (M i).trace
@[simp]
theorem Matrix.trace_sub {n : Type u_3} {R : Type u_6} [] [] (A : Matrix n n R) (B : Matrix n n R) :
(A - B).trace = A.trace - B.trace
@[simp]
theorem Matrix.trace_neg {n : Type u_3} {R : Type u_6} [] [] (A : Matrix n n R) :
(-A).trace = -A.trace
@[simp]
theorem Matrix.trace_one {n : Type u_3} {R : Type u_6} [] [] :
= ()
@[simp]
theorem Matrix.trace_transpose_mul {m : Type u_2} {n : Type u_3} {R : Type u_6} [] [] [] [Mul R] (A : Matrix m n R) (B : Matrix n m R) :
(A.transpose * B.transpose).trace = (A * B).trace
theorem Matrix.trace_mul_comm {m : Type u_2} {n : Type u_3} {R : Type u_6} [] [] [] [] (A : Matrix m n R) (B : Matrix n m R) :
(A * B).trace = (B * A).trace
theorem Matrix.trace_mul_cycle {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_6} [] [] [] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R) :
(A * B * C).trace = (C * A * B).trace
theorem Matrix.trace_mul_cycle' {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_6} [] [] [] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R) :
(A * (B * C)).trace = (C * (A * B)).trace
@[simp]
theorem Matrix.trace_col_mul_row {n : Type u_3} {R : Type u_6} [] {ι : Type u_8} [] (a : nR) (b : nR) :
( * ).trace =
theorem Matrix.trace_submatrix_succ {R : Type u_6} {n : } (M : Matrix (Fin n.succ) (Fin n.succ) R) :
M 0 0 + (M.submatrix Fin.succ Fin.succ).trace = M.trace

Special cases for Fin n#

While simp [Fin.sum_univ_succ] can prove these, we include them for convenience and consistency with Matrix.det_fin_two etc.

theorem Matrix.trace_fin_zero {R : Type u_6} [] (A : Matrix (Fin 0) (Fin 0) R) :
A.trace = 0
theorem Matrix.trace_fin_one {R : Type u_6} [] (A : Matrix (Fin 1) (Fin 1) R) :
A.trace = A 0 0
theorem Matrix.trace_fin_two {R : Type u_6} [] (A : Matrix (Fin 2) (Fin 2) R) :
A.trace = A 0 0 + A 1 1
theorem Matrix.trace_fin_three {R : Type u_6} [] (A : Matrix (Fin 3) (Fin 3) R) :
A.trace = A 0 0 + A 1 1 + A 2 2