Hermitian_Matrix_has_Real_Eigenvalues
Provedeigenvalueshermitian-matriceslinear-algebraproofwiki
Every Hermitian matrix has eigenvalues which are all real numbers.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.LinearAlgebra.Matrix.Hermitian
Formal statement
theorem Hermitian_Matrix_has_Real_Eigenvalues {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) (hA : A.IsHermitian) (μ : ℂ) (hμ : ∃ v : Fin n → ℂ, v ≠ 0 ∧ A.mulVec v = μ • v) : μ.im = 0 := by sorrySource