Theorem: chapter07.Theorem₁ (FormalBook/Chapter_07.lean)

State before:
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
h : A.IsHermitian
⊢ ∃ Q ∈ orthogonalGroup (Fin n) ℝ, ∃ d, diagonal d = Q.conjTranspose * A * Q
Tactic:
sorry
State after:
no goals