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
The trace of a square matrix. For more bundled versions, see:
Equations
- A.trace = ∑ i : n, A.diag i
Instances For
theorem
Matrix.trace_diagonal
{R : Type u_6}
[AddCommMonoid R]
{o : Type u_8}
[Fintype o]
[DecidableEq o]
(d : o → R)
:
(Matrix.diagonal d).trace = ∑ i : o, d i
@[simp]
theorem
Matrix.trace_zero
(n : Type u_3)
(R : Type u_6)
[Fintype n]
[AddCommMonoid R]
:
Matrix.trace 0 = 0
@[simp]
theorem
Matrix.trace_eq_zero_of_isEmpty
{n : Type u_3}
{R : Type u_6}
[Fintype n]
[AddCommMonoid R]
[IsEmpty n]
(A : Matrix n n R)
:
A.trace = 0
@[simp]
theorem
Matrix.trace_smul
{n : Type u_3}
{α : Type u_5}
{R : Type u_6}
[Fintype n]
[AddCommMonoid R]
[Monoid α]
[DistribMulAction α R]
(r : α)
(A : Matrix n n R)
:
@[simp]
theorem
Matrix.trace_transpose
{n : Type u_3}
{R : Type u_6}
[Fintype n]
[AddCommMonoid R]
(A : Matrix n n R)
:
A.transpose.trace = A.trace
@[simp]
theorem
Matrix.trace_conjTranspose
{n : Type u_3}
{R : Type u_6}
[Fintype n]
[AddCommMonoid R]
[StarAddMonoid R]
(A : Matrix n n R)
:
@[simp]
theorem
Matrix.traceAddMonoidHom_apply
(n : Type u_3)
(R : Type u_6)
[Fintype n]
[AddCommMonoid R]
(A : Matrix n n R)
:
(Matrix.traceAddMonoidHom n R) A = A.trace
Matrix.trace
as an AddMonoidHom
Equations
- Matrix.traceAddMonoidHom n R = { 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)
[Fintype n]
[AddCommMonoid R]
[Semiring α]
[Module α R]
(A : Matrix n n R)
:
(Matrix.traceLinearMap n α R) A = A.trace
def
Matrix.traceLinearMap
(n : Type u_3)
(α : Type u_5)
(R : Type u_6)
[Fintype n]
[AddCommMonoid R]
[Semiring α]
[Module α R]
:
Matrix.trace
as a LinearMap
Equations
- Matrix.traceLinearMap n α R = { toFun := Matrix.trace, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
Matrix.trace_list_sum
{n : Type u_3}
{R : Type u_6}
[Fintype n]
[AddCommMonoid R]
(l : List (Matrix n n R))
:
@[simp]
theorem
Matrix.trace_multiset_sum
{n : Type u_3}
{R : Type u_6}
[Fintype n]
[AddCommMonoid R]
(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}
[Fintype n]
[AddCommMonoid R]
(s : Finset ι)
(f : ι → Matrix n n R)
:
(∑ i ∈ s, f i).trace = ∑ i ∈ s, (f i).trace
theorem
AddMonoidHom.map_trace
{n : Type u_3}
{R : Type u_6}
{S : Type u_7}
[Fintype n]
[AddCommMonoid R]
[AddCommMonoid S]
(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}
[Fintype n]
[Fintype p]
[AddCommMonoid R]
[DecidableEq p]
(M : p → Matrix n n R)
:
(Matrix.blockDiagonal M).trace = ∑ i : p, (M i).trace
theorem
Matrix.trace_blockDiagonal'
{p : Type u_4}
{R : Type u_6}
[Fintype p]
[AddCommMonoid R]
[DecidableEq p]
{m : p → Type u_8}
[(i : p) → Fintype (m i)]
(M : (i : p) → Matrix (m i) (m i) R)
:
(Matrix.blockDiagonal' M).trace = ∑ i : p, (M i).trace
@[simp]
theorem
Matrix.trace_neg
{n : Type u_3}
{R : Type u_6}
[Fintype n]
[AddCommGroup R]
(A : Matrix n n R)
:
@[simp]
theorem
Matrix.trace_one
{n : Type u_3}
{R : Type u_6}
[Fintype n]
[DecidableEq n]
[AddCommMonoidWithOne R]
:
Matrix.trace 1 = ↑(Fintype.card n)
theorem
Matrix.trace_mul_comm
{m : Type u_2}
{n : Type u_3}
{R : Type u_6}
[Fintype m]
[Fintype n]
[AddCommMonoid R]
[CommSemigroup R]
(A : Matrix m n R)
(B : Matrix n m R)
:
@[simp]
theorem
Matrix.trace_col_mul_row
{n : Type u_3}
{R : Type u_6}
[Fintype n]
{ι : Type u_8}
[Unique ι]
[NonUnitalNonAssocSemiring R]
(a : n → R)
(b : n → R)
:
(Matrix.col ι a * Matrix.row ι b).trace = Matrix.dotProduct a b
theorem
Matrix.trace_submatrix_succ
{R : Type u_6}
{n : ℕ}
[NonUnitalNonAssocSemiring R]
(M : Matrix (Fin n.succ) (Fin n.succ) R)
:
@[simp]
theorem
Matrix.trace_fin_zero
{R : Type u_6}
[AddCommMonoid R]
(A : Matrix (Fin 0) (Fin 0) R)
:
A.trace = 0
theorem
Matrix.trace_fin_one
{R : Type u_6}
[AddCommMonoid R]
(A : Matrix (Fin 1) (Fin 1) R)
:
A.trace = A 0 0
@[simp]
@[simp]
@[simp]
theorem
Matrix.trace_fin_three_of
{R : Type u_6}
[AddCommMonoid R]
(a : R)
(b : R)
(c : R)
(d : R)
(e : R)
(f : R)
(g : R)
(h : R)
(i : R)
: