Completion of an algebraic closure of a p-adic field is algebraically closed (source code)

= Completion of an algebraic closure of a p-adic field is algebraically closed
{title2=$\mathbb C_p$ is algebraically closed}

The completion $\mathbb C_p$ of an <algebraic closure> of $\mathbb Q_p$ is an <algebraically closed field>. Approximate a polynomial over $\mathbb C_p$ by one over $\overline{\mathbb Q}_p$, use <continuity of roots over a non-Archimedean field> to obtain a nearby algebraic root, and then use <Krasner's lemma> to show that the original root already belongs to $\mathbb C_p$.