Spectral theorem for normal operators (source code)

= Spectral theorem for normal operators

Every normal operator on a finite-dimensional complex inner-product space has an orthonormal basis of eigenvectors. An eigenvector is also an eigenvector of the adjoint with conjugate eigenvalue, so its orthogonal complement reduces the operator and induction applies.