trace_eq_sum_eigenvalues — Mathlib

English

The trace of a Hermitian matrix equals the sum of its eigenvalues.

Русский

След эрмитовой матрицы равен сумме её собственных значений.

LaTeX

$$$\\\\operatorname{tr}(A) = \\\\sum_i h_A\\\\,\\\\mathrm{eigenvalues}_i$$$

Lean4

theorem trace_eq_sum_eigenvalues [DecidableEq n] (hA : A.IsHermitian) : A.trace = ∑ i, (hA.eigenvalues i : 𝕜) := by
  simp [trace_eq_sum_roots_charpoly_of_splits hA.splits_charpoly, hA.roots_charpoly_eq_eigenvalues]

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