mathlib3 documentation

linear_algebra.matrix.trace

Trace of a matrix #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

See also linear_algebra.trace for the trace of an endomorphism.

Tags #

matrix, trace, diagonal

source
def matrix.trace {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_monoid R] (A : matrix n n R) :
R

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

Equations
source
@[simp]
theorem matrix.trace_zero (n : Type u_3) (R : Type u_6) [fintype n] [add_comm_monoid R] :
0.trace = 0
source
@[simp]
theorem matrix.trace_add {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_monoid R] (A B : matrix n n R) :
(A + B).trace = A.trace + B.trace
source
@[simp]
theorem matrix.trace_smul {n : Type u_3} {α : Type u_5} {R : Type u_6} [fintype n] [add_comm_monoid R] [monoid α] [distrib_mul_action α R] (r : α) (A : matrix n n R) :
(r • A).trace = r • A.trace
source
@[simp]
theorem matrix.trace_transpose {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_monoid R] (A : matrix n n R) :
A.transpose.trace = A.trace
source
@[simp]
theorem matrix.trace_conj_transpose {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_monoid R] [star_add_monoid R] (A : matrix n n R) :
A.conj_transpose.trace = has_star.star A.trace
source
def matrix.trace_add_monoid_hom (n : Type u_3) (R : Type u_6) [fintype n] [add_comm_monoid R] :
matrix n n R →+ R

matrix.trace as an add_monoid_hom

Equations
source
@[simp]
theorem matrix.trace_add_monoid_hom_apply (n : Type u_3) (R : Type u_6) [fintype n] [add_comm_monoid R] (A : matrix n n R) :
⇑(matrix.trace_add_monoid_hom n R) A = A.trace
source
@[simp]
theorem matrix.trace_linear_map_apply (n : Type u_3) (α : Type u_5) (R : Type u_6) [fintype n] [add_comm_monoid R] [semiring α] [module α R] (A : matrix n n R) :
⇑(matrix.trace_linear_map n α R) A = A.trace
source
def matrix.trace_linear_map (n : Type u_3) (α : Type u_5) (R : Type u_6) [fintype n] [add_comm_monoid R] [semiring α] [module α R] :
matrix n n R →ₗ[α] R

matrix.trace as a linear_map

Equations
source
@[simp]
theorem matrix.trace_list_sum {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_monoid R] (l : list (matrix n n R)) :
l.sum.trace = (list.map matrix.trace l).sum
source
@[simp]
theorem matrix.trace_multiset_sum {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_monoid R] (s : multiset (matrix n n R)) :
s.sum.trace = (multiset.map matrix.trace s).sum
source
@[simp]
theorem matrix.trace_sum {ι : Type u_1} {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_monoid R] (s : finset ι) (f : ι → matrix n n R) :
(s.sum (λ (i : ι), f i)).trace = s.sum (λ (i : ι), (f i).trace)
source
@[simp]
theorem matrix.trace_sub {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_group R] (A B : matrix n n R) :
(A - B).trace = A.trace - B.trace
source
@[simp]
theorem matrix.trace_neg {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_group R] (A : matrix n n R) :
(-A).trace = -A.trace
source
@[simp]
theorem matrix.trace_one {n : Type u_3} {R : Type u_6} [fintype n] [decidable_eq n] [add_comm_monoid_with_one R] :
1.trace = ↑(fintype.card n)
source
@[simp]
theorem matrix.trace_transpose_mul {m : Type u_2} {n : Type u_3} {R : Type u_6} [fintype m] [fintype n] [add_comm_monoid R] [has_mul R] (A : matrix m n R) (B : matrix n m R) :
(A.transpose.mul B.transpose).trace = (A.mul B).trace
source
theorem matrix.trace_mul_comm {m : Type u_2} {n : Type u_3} {R : Type u_6} [fintype m] [fintype n] [add_comm_monoid R] [comm_semigroup R] (A : matrix m n R) (B : matrix n m R) :
(A.mul B).trace = (B.mul A).trace
source
theorem matrix.trace_mul_cycle {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_6} [fintype m] [fintype n] [fintype p] [non_unital_comm_semiring R] (A : matrix m n R) (B : matrix n p R) (C : matrix p m R) :
((A.mul B).mul C).trace = ((C.mul A).mul B).trace
source
theorem matrix.trace_mul_cycle' {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_6} [fintype m] [fintype n] [fintype p] [non_unital_comm_semiring R] (A : matrix m n R) (B : matrix n p R) (C : matrix p m R) :
(A.mul (B.mul C)).trace = (C.mul (A.mul B)).trace
source
@[simp]
theorem matrix.trace_col_mul_row {n : Type u_3} {R : Type u_6} [fintype n] [non_unital_non_assoc_semiring R] (a b : n → R) :
((matrix.col a).mul (matrix.row b)).trace = matrix.dot_product a b

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.

source
@[simp]
theorem matrix.trace_fin_zero {R : Type u_6} [add_comm_monoid R] (A : matrix (fin 0) (fin 0) R) :
A.trace = 0
source
theorem matrix.trace_fin_one {R : Type u_6} [add_comm_monoid R] (A : matrix (fin 1) (fin 1) R) :
A.trace = A 0 0
source
theorem matrix.trace_fin_two {R : Type u_6} [add_comm_monoid R] (A : matrix (fin 2) (fin 2) R) :
A.trace = A 0 0 + A 1 1
source
theorem matrix.trace_fin_three {R : Type u_6} [add_comm_monoid R] (A : matrix (fin 3) (fin 3) R) :
A.trace = A 0 0 + A 1 1 + A 2 2