Normal spectral theorem

normal_spectral_theorem

Submitter: Kim Morrison.

Notes: A complex matrix A is normal (IsStarNormal A, i.e. Aᴴ A = A Aᴴ) iff it is unitarily diagonalizable, A = U (diagonal d) Uᴴ with U unitary. Mathlib has the Hermitian special case (Matrix.IsHermitian.spectral_theorem) and all conjugation/diagonal machinery, but not the normal generalization (no Matrix.IsStarNormal.spectral_theorem). The forward implication (a normal matrix admits an orthonormal eigenbasis) is the substantive content; the converse is a short computation. No new definitions beyond IsStarNormal, unitary, and Matrix.diagonal. Category-(b) candidate.

Source: Knill, *Some fundamental theorems in mathematics*, §14.

Informal solution: Forward: a normal matrix commutes with its conjugate transpose, so by simultaneous unitary triangularization (Schur) the triangular factor is itself normal, hence diagonal; the columns of the Schur unitary form an orthonormal eigenbasis, giving A = U (diagonal d) Uᴴ. Reverse: if A = U (diagonal d) Uᴴ with U unitary, then Aᴴ = U (diagonal d̄) Uᴴ and the two diagonal matrices commute, so A and Aᴴ commute, i.e. A is normal.

theorem declaration uses `sorry`normal_spectral_theorem (A : Matrix n n ℂ) :
    IsStarNormal A ↔
      ∃ U ∈ unitary (Matrix n n ℂ), ∃ d : n → ℂ,
        A = U * diagonal d * star U := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℂ⊢ IsStarNormal A ↔ ∃ U ∈ unitary (Matrix n n ℂ), ∃ d, A = U * diagonal d * star U
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 21, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 22, 2026

• @lukerj00 with Tau (caj.al) on Jun 25, 2026