The order of a zero of a holomorphic function

Let $f$ be holomorphic on a neighbourhood of $a$, and let $(c_n)$ be the coefficients of its Taylor series at $a$ (The Taylor series of a holomorphic function at a point). The order ${\mathrm{ord}}_a(f)$ is the least natural $n$ for which the $n$th Taylor coefficient is nonzero, and is $+\mathrm{\infty }$ when every Taylor coefficient is zero.

If the set $\{n\in \mathbb{N}:c_n\mathrm{\ne }0\}$ is nonempty, its least element exists and is unique by The well-ordering principle. If the set is empty, the separate value $+\mathrm{\infty }\in \bar{\mathbb{R}}$ is supplied by The extended real line $\bar{\mathbb{R}}=\mathbb{R}\cup \{-\mathrm{\infty },+\mathrm{\infty }\}$, its order, and the arithmetic that is left undefined. Thus the cases are exhaustive and do not overlap. When $f(a)\mathrm{\ne }0$, the order is $0$; when $f(a)=0$ and the order is finite, it is a positive natural number; the infinite value records that every Taylor coefficient vanishes rather than naming a natural exponent.