Hermitian matrices: the trace is real

Mathlib candidate for Mathlib/LinearAlgebra/Matrix/Hermitian.lean. Mathlib has Matrix.IsHermitian.trace_eq_sum_eigenvalues (in Mathlib.Analysis.Matrix.Spectrum), which implies this through the spectral theorem; the statement here needs only the diagonal entries and no spectral machinery.