 Spectral theorem for compact Hermitian operators

A compact Hermitian operator has real nonzero eigenvalues of finite multiplicity, with zero as their only possible accumulation point, and an orthonormal eigenbasis after a basis of its kernel is included.

This is the discrete-eigenbasis case of the spectral theorem for a compact operator that is self-adjoint.