Chapter 7, Theorem 1: spectral theorem

Proved

BookSixth.spectral

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

Every real symmetric square matrix can be diagonalized by a real orthogonal change of basis. The dimension may be zero; the real unitary group is the orthogonal group.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.spectral {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsHermitian) :
    ∃ Q : Matrix.unitaryGroup (Fin n) ℝ, ∃ d : Fin n → ℝ,
      star (Q : Matrix (Fin n) (Fin n) ℝ) * A * (Q : Matrix (Fin n) (Fin n) ℝ) = Matrix.diagonal d := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 7, Theorem 1: spectral theorem, p. 39. https://doi.org/10.1007/978-3-662-57265-8_7

View graph