re_trace_eq_sum_eigenvalues — Mathlib

English

In finite-dimensional real inner product spaces, for a symmetric T, the real part of the trace equals the sum of eigenvalues; equivalently Tr(T) equals sum of eigenvalues since eigenvalues are real.

Русский

В конечномерном вещественном пространстве для симметричного T след T равен сумме собственных значений; эквивалентно, Tr(T) равно сумме собственных значений, поскольку они вещественные.

LaTeX

$$Tr(T) = \sum_i λ_i$$

Lean4

theorem re_trace_eq_sum_eigenvalues {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
    RCLike.re (T.trace 𝕜 E) = ∑ i, hT.eigenvalues hn i :=
  by
  rw [hT.trace_eq_sum_eigenvalues]
  exact RCLike.ofReal_re_ax _

Похожие утверждения