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_4)
(M : Type u_5)
[semiring R]
[add_comm_monoid M]
[module R M] :
The diagonal of a square matrix.
@[simp]
theorem
matrix.diag_apply
{n : Type u_2}
{R : Type u_4}
{M : Type u_5}
[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_4}
[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_4}
{M : Type u_5}
[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
@[simp]
theorem
matrix.diag_col_mul_row
{n : Type u_2}
{R : Type u_4}
[semiring R]
(a b : n → R) :
⇑(matrix.diag n R R) (matrix.col a ⬝ matrix.row b) = a * b
def
matrix.trace
(n : Type u_2)
(R : Type u_4)
(M : Type u_5)
[semiring R]
[add_comm_monoid M]
[module R M]
[fintype n] :
The trace of a square matrix.
Equations
- matrix.trace n R M = {to_fun := λ (A : matrix n n M), ∑ (i : n), ⇑(matrix.diag n R M) A i, map_add' := _, map_smul' := _}
@[simp]
theorem
matrix.trace_diag
{n : Type u_2}
{R : Type u_4}
{M : Type u_5}
[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_4}
{M : Type u_5}
[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_4}
[semiring R]
[fintype n]
[decidable_eq n] :
⇑(matrix.trace n R R) 1 = ↑(fintype.card n)
@[simp]
theorem
matrix.trace_transpose
{n : Type u_2}
{R : Type u_4}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
[fintype n]
(A : matrix n n M) :
⇑(matrix.trace n R M) Aᵀ = ⇑(matrix.trace n R M) A
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 m S S) (A ⬝ B) = ⇑(matrix.trace n S S) (B ⬝ A)
theorem
matrix.trace_mul_cycle
{m : Type u_1}
{n : Type u_2}
{p : Type u_3}
[fintype n]
[fintype m]
[fintype p]
{S : Type v}
[comm_semiring S]
(A : matrix m n S)
(B : matrix n p S)
(C : matrix p m S) :
⇑(matrix.trace m S S) (A ⬝ B ⬝ C) = ⇑(matrix.trace p S S) (C ⬝ A ⬝ B)
theorem
matrix.trace_mul_cycle'
{m : Type u_1}
{n : Type u_2}
{p : Type u_3}
[fintype n]
[fintype m]
[fintype p]
{S : Type v}
[comm_semiring S]
(A : matrix m n S)
(B : matrix n p S)
(C : matrix p m S) :
⇑(matrix.trace m S S) (A ⬝ (B ⬝ C)) = ⇑(matrix.trace p S S) (C ⬝ (A ⬝ B))
@[simp]
theorem
matrix.trace_col_mul_row
{n : Type u_2}
{R : Type u_4}
[semiring R]
[fintype n]
(a b : n → R) :
⇑(matrix.trace n R R) (matrix.col a ⬝ matrix.row b) = 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.
@[simp]
theorem
matrix.trace_fin_zero
{R : Type u_4}
[semiring R]
(A : matrix (fin 0) (fin 0) R) :
⇑(matrix.trace (fin 0) R R) A = 0
theorem
matrix.trace_fin_one
{R : Type u_4}
[semiring R]
(A : matrix (fin 1) (fin 1) R) :
⇑(matrix.trace (fin 1) R R) A = A 0 0