Abstract
This entry shows an important basic fact in complex analysis, namely that a complex-valued function $f$ holomorphic on an open annulus $\{z \mid 0\leq r < \Vert z - z_0\Vert \leq R\}$ has a (generalised) Laurent series expansion of the form \[f(z) = \sum_{n=-\infty}^\infty a_n (z - z_0)^n\] that is valid on the entire annulus.
An important special case that is also developed is $r = 0$, i.e. the local behaviour of a function around an isolated singularity. For non-essential singularities, this reduces to the well-known simpler Laurent series expansions from HOL-Complex_Analysis of the form $\sum_{n=n_0}^\infty a_n (z-z_0)^n$.