mathlib documentation

linear_algebra.matrix.trace

Trace of a matrix #

This file defines the trace of a matrix, the linear 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.diag (n : Type u_2) (R : Type u_3) (M : Type u_4) [semiring R] [add_comm_monoid M] [module R M] :
matrix n n M →ₗ[R] n → M

The diagonal of a square matrix.

Equations
@[simp]
theorem matrix.diag_apply {n : Type u_2} {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (A : matrix n n M) (i : n) :
(matrix.diag n R M) A i = A i i
@[simp]
theorem matrix.diag_one {n : Type u_2} {R : Type u_3} [semiring R] [decidable_eq n] :
(matrix.diag n R R) 1 = λ (i : n), 1
@[simp]
theorem matrix.diag_transpose {n : Type u_2} {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (A : matrix n n M) :
(matrix.diag n R M) A = (matrix.diag n R M) A
def matrix.trace (n : Type u_2) (R : Type u_3) (M : Type u_4) [semiring R] [add_comm_monoid M] [module R M] [fintype n] :
matrix n n M →ₗ[R] M

The trace of a square matrix.

Equations
@[simp]
theorem matrix.trace_diag {n : Type u_2} {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [fintype n] (A : matrix n n M) :
(matrix.trace n R M) A = ∑ (i : n), (matrix.diag n R M) A i
theorem matrix.trace_apply {n : Type u_2} {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [fintype n] (A : matrix n n M) :
(matrix.trace n R M) A = ∑ (i : n), A i i
@[simp]
theorem matrix.trace_one {n : Type u_2} {R : Type u_3} [semiring R] [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.trace_transpose {n : Type u_2} {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [fintype n] (A : matrix n n M) :
@[simp]
theorem matrix.trace_transpose_mul {m : Type u_1} {n : Type u_2} {R : Type u_3} [semiring R] [fintype n] [fintype m] (A : matrix m n R) (B : matrix n m R) :
(matrix.trace n R R) (A B) = (matrix.trace m R R) (A B)
theorem matrix.trace_mul_comm {m : Type u_1} {n : Type u_2} [fintype n] [fintype m] {S : Type v} [comm_semiring S] (A : matrix m n S) (B : matrix n m S) :
(matrix.trace n S S) (B A) = (matrix.trace m S S) (A B)