Coprime factor lifting from valuation-extension uniqueness (source code)

= Coprime factor lifting from valuation-extension uniqueness

Suppose a <Non-Archimedean absolute value> on $K$ has a unique <extension of an absolute value> to every finite extension. Factor a <monic> $g\in\mathcal O_K[X]$ into <monic> irreducible factors over $K$. All factors have integral coefficients because their roots have absolute value at most one. By <pure-power reduction of a monic irreducible polynomial>, each factor reduces to a power of a single irreducible <polynomial>. If $\overline g=\overline g_1\overline g_2$ is a <coprime> <monic> factorization, assign each whole irreducible factor of $g$, with its multiplicity, to the unique side containing its residue factor. The resulting <monic> $g_1,g_2\in\mathcal O_K[X]$ satisfy $g=g_1g_2$ and reduce to the prescribed factors. Completeness of $K$ is not required for this proof.