Pure-power reduction of a monic irreducible polynomial (source code)

= Pure-power reduction of a monic irreducible polynomial
{title2=$\overline f=\varphi^m$}

Suppose a <Non-Archimedean absolute value> extends uniquely to every finite extension. If $f\in\mathcal O_K[X]$ is <monic> and irreducible, every root has absolute value at most one: otherwise its leading power dominates all lower terms, contradicting $f(\alpha)=0$ by the <ultrametric inequality>. In a <splitting field>, let $\varphi$ be the <minimal polynomial of an algebraic element> of the residue of one root. Lift its coefficients to $\mathcal O_K$. The lift has absolute value less than one at that root and hence, by <equal absolute values of algebraic conjugates>, at every root. Consequently every root residue is a zero of $\varphi$. Since reduction preserves the product of the linear factors with multiplicities, every irreducible factor of $\overline f$ is $\varphi$, proving the displayed identity for some $m\geq1$.