Project idea: spectral theorem for normal endomorphisms

Stream: LFTCM 2024

[Jireh Loreaux]

The goal is to show that the normal endomorphisms on a finite dimensional inner product space over ℝ or ℂ are diagonalizable (i.e., the space is the direct sum of orthogonal eigenspaces). Mathlib already knows this for symmetric endomorphisms, but it doesn't have this generalization.