Finite-rank Fredholm alternative (source code)

= Finite-rank Fredholm alternative

For a finite-rank operator $S$ and $\lambda\ne0$, if $\lambda$ is not an eigenvalue then $S-\lambda I$ is surjective. Decompose the Hilbert space into $\operatorname{im}S$ and its orthogonal complement, then use injectivity and surjectivity equivalence on the finite-dimensional image.