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

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
@[simp]
theorem matrix.trace_zero (n : Type u_3) (R : Type u_6) [fintype n] [add_comm_monoid R] :
0.trace = 0
@[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
@[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
@[simp]
theorem matrix.trace_transpose {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_monoid R] (A : matrix n n R) :
@[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) :
@[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) :
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
@[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)) :
@[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)) :
@[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)
@[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
@[simp]
theorem matrix.trace_neg {n : Type u_3} {R : Type u_6} [fintype n] [add_comm_group R] (A : matrix n n R) :
@[simp]
theorem matrix.trace_one {n : Type u_3} {R : Type u_6} [fintype n] [decidable_eq n] [add_comm_monoid_with_one R] :
@[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) :
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
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
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
@[simp]

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.

@[simp]
theorem matrix.trace_fin_zero {R : Type u_6} [add_comm_monoid R] (A : matrix (fin 0) (fin 0) R) :
A.trace = 0
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
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
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