Documentation

Mathlib.LinearAlgebra.Matrix.Trace

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

source
def Matrix.trace {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] (A : Matrix n n R) :
R

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

Equations
Instances For
    source
    @[simp]
    theorem Matrix.trace_diagonal {R : Type u_6} [AddCommMonoid R] {o : Type u_8} [Fintype o] [DecidableEq o] (d : o → R) :
    (diagonal d).trace = ∑ i : o, d i
    source
    @[simp]
    theorem Matrix.trace_zero (n : Type u_3) (R : Type u_6) [Fintype n] [AddCommMonoid R] :
    trace 0 = 0
    source
    @[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
    source
    @[simp]
    theorem Matrix.trace_add {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid 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] [AddCommMonoid R] [DistribSMul α 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] [AddCommMonoid R] (A : Matrix n n R) :
    A.transpose.trace = A.trace
    source
    @[simp]
    theorem Matrix.trace_conjTranspose {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] [StarAddMonoid R] (A : Matrix n n R) :
    A.conjTranspose.trace = star A.trace
    source
    def Matrix.traceAddMonoidHom (n : Type u_3) (R : Type u_6) [Fintype n] [AddCommMonoid R] :
    Matrix n n R →+ R

    Matrix.trace as an AddMonoidHom

    Equations
    Instances For
      source
      @[simp]
      theorem Matrix.traceAddMonoidHom_apply (n : Type u_3) (R : Type u_6) [Fintype n] [AddCommMonoid R] (A : Matrix n n R) :
      (traceAddMonoidHom n R) A = A.trace
      source
      def Matrix.traceLinearMap (n : Type u_3) (α : Type u_5) (R : Type u_6) [Fintype n] [AddCommMonoid R] [Semiring α] [Module α R] :
      Matrix n n R →ₗ[α] R

      Matrix.trace as a LinearMap

      Equations
      Instances For
        source
        @[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) :
        (traceLinearMap n α R) A = A.trace
        source
        @[simp]
        theorem Matrix.trace_list_sum {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] (l : List (Matrix n n R)) :
        l.sum.trace = (List.map trace l).sum
        source
        @[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 trace s).sum
        source
        @[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
        source
        theorem AddMonoidHom.map_trace {n : Type u_3} {R : Type u_6} {S : Type u_7} [Fintype n] [AddCommMonoid R] [AddCommMonoid S] {F : Type u_8} [FunLike F R S] [AddMonoidHomClass F R S] (f : F) (A : Matrix n n R) :
        f A.trace = (A.map ⇑f).trace
        source
        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) :
        (blockDiagonal M).trace = ∑ i : p, (M i).trace
        source
        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) :
        (blockDiagonal' M).trace = ∑ i : p, (M i).trace
        source
        @[simp]
        theorem Matrix.trace_sub {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommGroup 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] [AddCommGroup 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] [DecidableEq n] [AddCommMonoidWithOne R] :
        trace 1 = ↑(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] [AddCommMonoid R] [Mul R] (A : Matrix m n R) (B : Matrix n m R) :
        (A.transpose * B.transpose).trace = (A * B).trace
        source
        theorem Matrix.trace_mul_comm {m : Type u_2} {n : Type u_3} {R : Type u_6} [Fintype m] [Fintype n] [AddCommMonoid R] [CommMagma R] (A : Matrix m n R) (B : Matrix n m R) :
        (A * B).trace = (B * 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] [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R) :
        (A * B * C).trace = (C * A * 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] [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R) :
        (A * (B * C)).trace = (C * (A * B)).trace
        source
        theorem Matrix.trace_mul_pow_comm_of_ne_zero {m : Type u_2} {n : Type u_3} {R : Type u_6} [Fintype m] [Fintype n] [CommSemiring R] [DecidableEq m] [DecidableEq n] (A : Matrix m n R) (B : Matrix n m R) {k : ℕ} (hk : k ≠ 0) :
        ((A * B) ^ k).trace = ((B * A) ^ k).trace

        The trace of a positive power of A * B is unchanged when the factors are reversed. The matrices A and B may be rectangular.

        This requires a positive exponent because the identity does not hold at exponent zero when the index types have different cardinalities.

        source
        theorem Matrix.trace_mul_pow_comm {n : Type u_3} {R : Type u_6} [Fintype n] [CommSemiring R] [DecidableEq n] (A B : Matrix n n R) (k : ℕ) :
        ((A * B) ^ k).trace = ((B * A) ^ k).trace

        For square matrices, the trace of any power of A * B is unchanged when the factors are reversed.

        Unlike the rectangular version trace_mul_pow_comm_of_ne_zero, this also holds at exponent zero.

        source
        @[simp]
        theorem Matrix.trace_replicateCol_mul_replicateRow {n : Type u_3} {R : Type u_6} [Fintype n] {ι : Type u_8} [Unique ι] [NonUnitalNonAssocSemiring R] (a b : n → R) :
        (replicateCol ι a * replicateRow ι b).trace = a ⬝ᵥ b
        source
        @[simp]
        theorem Matrix.trace_vecMulVec {n : Type u_3} {R : Type u_6} [Fintype n] [NonUnitalNonAssocSemiring R] (a b : n → R) :
        (vecMulVec a b).trace = a ⬝ᵥ b
        source
        theorem Matrix.trace_submatrix_succ {R : Type u_6} {n : ℕ} [AddCommMonoid R] (M : Matrix (Fin n.succ) (Fin n.succ) R) :
        M 0 0 + (M.submatrix Fin.succ Fin.succ).trace = M.trace
        source
        theorem Matrix.trace_units_conj {m : Type u_2} {R : Type u_6} [Fintype m] [DecidableEq m] [CommSemiring R] (M : (Matrix m m R)ˣ) (N : Matrix m m R) :
        (↑M * N * ↑M⁻¹).trace = N.trace
        source
        theorem Matrix.trace_units_conj' {m : Type u_2} {R : Type u_6} [Fintype m] [DecidableEq m] [CommSemiring R] (M : (Matrix m m R)ˣ) (N : Matrix m m R) :
        (↑M⁻¹ * N * ↑M).trace = N.trace

        The trace is invariant under conjugation by a unit, variant of Matrix.trace_units_conj with the inverse on the left.

        Special cases for Fin n for low values of n #

        source
        @[simp]
        theorem Matrix.trace_fin_zero {R : Type u_6} [AddCommMonoid R] (A : Matrix (Fin 0) (Fin 0) R) :
        A.trace = 0
        source
        theorem Matrix.trace_fin_one {R : Type u_6} [AddCommMonoid R] (A : Matrix (Fin 1) (Fin 1) R) :
        A.trace = A 0 0
        source
        theorem Matrix.trace_fin_two {R : Type u_6} [AddCommMonoid 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} [AddCommMonoid R] (A : Matrix (Fin 3) (Fin 3) R) :
        A.trace = A 0 0 + A 1 1 + A 2 2
        source
        @[simp]
        theorem Matrix.trace_fin_one_of {R : Type u_6} [AddCommMonoid R] (a : R) :
        !![a].trace = a
        source
        @[simp]
        theorem Matrix.trace_fin_two_of {R : Type u_6} [AddCommMonoid R] (a b c d : R) :
        !![a, b; c, d].trace = a + d
        source
        @[simp]
        theorem Matrix.trace_fin_three_of {R : Type u_6} [AddCommMonoid R] (a b c d e f g h i : R) :
        !![a, b, c; d, e, f; g, h, i].trace = a + e + i
        source
        @[simp]
        theorem Matrix.trace_single_eq_of_ne {n : Type u_9} {α : Type u_11} [DecidableEq n] [Fintype n] [AddCommMonoid α] (i j : n) (c : α) (h : i ≠ j) :
        (single i j c).trace = 0
        source
        @[simp]
        theorem Matrix.trace_single_eq_same {n : Type u_9} {α : Type u_11} [DecidableEq n] [Fintype n] [AddCommMonoid α] (i : n) (c : α) :
        (single i i c).trace = c
        source
        theorem Matrix.trace_single_mul {m : Type u_8} {n : Type u_9} {R : Type u_10} [DecidableEq m] [DecidableEq n] [Fintype n] [NonUnitalNonAssocSemiring R] [Fintype m] (i : n) (j : m) (a : R) (x : Matrix m n R) :
        (single i j a * x).trace = a • x j i
        source
        theorem Matrix.trace_mul_single {m : Type u_8} {n : Type u_9} {R : Type u_10} [DecidableEq m] [DecidableEq n] [Fintype n] [NonUnitalNonAssocSemiring R] [Fintype m] (x : Matrix m n R) (i : n) (j : m) (a : R) :
        (x * single i j a).trace = MulOpposite.op a • x j i
        source
        theorem Matrix.trace_surjective {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] [Nonempty n] :
        Function.Surjective trace
        source
        theorem Matrix.ext_iff_trace_mul_left {m : Type u_2} {n : Type u_3} {R : Type u_6} [Fintype m] [Fintype n] [NonAssocSemiring R] {A B : Matrix m n R} :
        A = B ↔ ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace

        Matrices A and B are equal iff (x * A).trace = (x * B).trace for all x.

        source
        theorem Matrix.ext_iff_trace_mul_right {m : Type u_2} {n : Type u_3} {R : Type u_6} [Fintype m] [Fintype n] [NonAssocSemiring R] {A B : Matrix m n R} :
        A = B ↔ ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace

        Matrices A and B are equal iff (A * x).trace = (B * x).trace for all x.