 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.