theorem SpectralTheorem.normal_complex_unitarily_diagonalizable {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℂ) (hM : IsStarNormal M) : ∃ (P : Matrix n n ℂ) (_ : P ∈ Matrix.unitaryGroup n ℂ) (d : n → ℂ), star P * M * P = Matrix.diagonal d

theorem SpectralTheorem.spectral_theorem {n : Type u_1} [Fintype n] [DecidableEq n] : (∀ (M : Matrix n n ℂ), IsStarNormal M → ∃ (P : Matrix n n ℂ) (_ : P ∈ Matrix.unitaryGroup n ℂ) (d : n → ℂ), star P * M * P = Matrix.diagonal d) ∧ (∀ (M : Matrix n n ℝ), M.IsSymm → ∃ (P : Matrix n n ℝ) (_ : P ∈ Matrix.unitaryGroup n ℝ) (d : n → ℝ), star P * M * P = Matrix.diagonal d) ∧ ∀ (M : Matrix n n ℂ), M.IsHermitian → spectrum ℂ M ⊆ Set.range Complex.ofReal