Integral complex numbers lie in the integral closure of ℤ

Let $z$ be a complex number which is integral over $\mathbb{Z}$, i.e. $z$ is a root of some monic polynomial with integer coefficients. The assertion is that there exists an element $a$ of the subalgebra $\mathrm{integralClosure}\ \mathbb{Z}\ \mathbb{C}$ of $\mathbb{C}$, namely the subalgebra of those complex numbers integral over $\mathbb{Z}$, whose image under the coercion to $\mathbb{C}$ equals $z$. This is nothing more than a restatement of the hypothesis in existential form: it converts the predicate IsIntegral ℤ z into the existence of a preimage of $z$ under the inclusion of the integral closure into $\mathbb{C}$, which is the shape required when one wants to speak of $z$ as an element of the ring of algebraic integers rather than as a complex number satisfying a property.

The statement records that the integral closure of $\mathbb{Z}$ in $\mathbb{C}$ is precisely the set of algebraic integers, in the packaged form needed downstream. It is used by CuspForm.IsNormalizedEigenform.exists_integralClosure_coe_eq_qCoeff, which exhibits the $q$-expansion coefficients of a normalised eigenform as elements of the ring of algebraic integers.