[proofplan] We reduce the problem to an application of Hensel's Lemma. A simple root $\bar{\alpha}$ of $\bar{f}$ yields a coprime factorisation $\bar{f}(x) = (x - \bar{\alpha}) \cdot \bar{h}(x)$ in $k_K[x]$, where coprimality follows from the simplicity of the root. Hensel's Lemma lifts this factorisation to $f(x) = (x - \alpha) \cdot h(x)$ in $\mathcal{O}_K[x]$ with $\alpha \equiv \bar{\alpha} \pmod{\mathfrak{m}_K}$. Uniqueness follows from the simplicity of $\bar{\alpha}$: any two lifts would give two distinct simple roots reducing to $\bar{\alpha}$, but the lifted factor $(x - \alpha)$ of degree 1 accounts for the unique root with this reduction. [/proofplan] [step:Factor $\bar{f}$ as $(x - \bar{\alpha}) \cdot \bar{h}(x)$ with coprime factors] Since $\bar{\alpha} \in k_K$ is a root of $\bar{f}$, the factor theorem in $k_K[x]$ gives a factorisation \begin{align*} \bar{f}(x) = (x - \bar{\alpha}) \cdot \bar{h}(x) \end{align*} for some monic polynomial $\bar{h} \in k_K[x]$ of degree $\deg \bar{f} - 1 = n - 1$. We verify the coprimality condition $\gcd(x - \bar{\alpha}, \bar{h}) = 1$ in $k_K[x]$. Since $\bar{\alpha}$ is a simple root of $\bar{f}$, the multiplicity of $\bar{\alpha}$ as a root of $\bar{f}$ is exactly 1. If $\bar{\alpha}$ were also a root of $\bar{h}$, then $(x - \bar{\alpha})$ would divide $\bar{h}(x)$, giving $(x - \bar{\alpha})^2 \mid \bar{f}(x)$, contradicting the simplicity of $\bar{\alpha}$. Therefore $\bar{h}(\bar{\alpha}) \neq 0$, which means $(x - \bar{\alpha})$ does not divide $\bar{h}(x)$. Since $(x - \bar{\alpha})$ is a linear (hence irreducible) polynomial, the only monic divisors of $(x - \bar{\alpha})$ are $1$ and $(x - \bar{\alpha})$ itself. Since $(x - \bar{\alpha}) \nmid \bar{h}$, we conclude $\gcd(x - \bar{\alpha}, \bar{h}) = 1$. [guided] We need to produce a coprime factorisation of $\bar{f}$ in $k_K[x]$ in order to apply [Hensel's Lemma](/theorems/???). The natural factorisation is to split off the root $\bar{\alpha}$. Since $\bar{\alpha}$ is a root of $\bar{f}$, the factor theorem gives $\bar{f}(x) = (x - \bar{\alpha}) \cdot \bar{h}(x)$ for some $\bar{h} \in k_K[x]$. Since $f$ is monic of degree $n$, its reduction $\bar{f}$ is monic of degree $n$ (the leading coefficient of $f$ is $1 \in \mathcal{O}_K^\times$, which reduces to $1 \in k_K^\times$), so $\bar{h}$ is monic of degree $n - 1$. Why is $\gcd(x - \bar{\alpha}, \bar{h}) = 1$? The polynomial $(x - \bar{\alpha})$ is linear, so irreducible in $k_K[x]$. The only way the gcd could be non-trivial is if $(x - \bar{\alpha})$ divides $\bar{h}(x)$, i.e., if $\bar{h}(\bar{\alpha}) = 0$. But if $\bar{h}(\bar{\alpha}) = 0$, then $(x - \bar{\alpha})^2$ divides $\bar{f}(x) = (x - \bar{\alpha})\bar{h}(x)$, making $\bar{\alpha}$ a repeated root. This contradicts the hypothesis that $\bar{\alpha}$ is a *simple* root of $\bar{f}$. Equivalently, the simplicity condition can be phrased in terms of the derivative: $\bar{\alpha}$ is a simple root of $\bar{f}$ if and only if $\bar{f}'(\bar{\alpha}) \neq 0$. Since $\bar{f}'(\bar{\alpha}) = \bar{h}(\bar{\alpha}) + (\bar{\alpha} - \bar{\alpha})\bar{h}'(\bar{\alpha}) = \bar{h}(\bar{\alpha})$ by the product rule, the condition $\bar{f}'(\bar{\alpha}) \neq 0$ is equivalent to $\bar{h}(\bar{\alpha}) \neq 0$, confirming coprimality. [/guided] [/step] [step:Apply Hensel's Lemma to lift the factorisation to $\mathcal{O}_K[x]$] The polynomial $f \in \mathcal{O}_K[x]$ is monic, hence primitive (the leading coefficient is $1$, which is a unit in $\mathcal{O}_K$, so $\max_i |a_i| = 1$). Its reduction $\bar{f} = (x - \bar{\alpha}) \cdot \bar{h}(x)$ is a coprime factorisation in $k_K[x]$ with $\deg(x - \bar{\alpha}) = 1$. By [Hensel's Lemma](/theorems/???), there exists a factorisation \begin{align*} f(x) = g(x) \cdot h(x) \quad \text{in } \mathcal{O}_K[x] \end{align*} with $g \equiv (x - \bar{\alpha}) \pmod{\mathfrak{m}_K}$, $h \equiv \bar{h} \pmod{\mathfrak{m}_K}$, and $\deg g = \deg(x - \bar{\alpha}) = 1$. Since $g$ is monic of degree 1 (it reduces to the monic polynomial $(x - \bar{\alpha})$ modulo $\mathfrak{m}_K$, and $\deg g = 1$), we may write $g(x) = x - \alpha$ for a unique $\alpha \in \mathcal{O}_K$. The congruence $g \equiv (x - \bar{\alpha}) \pmod{\mathfrak{m}_K}$ gives $\alpha \equiv \bar{\alpha} \pmod{\mathfrak{m}_K}$. Since $f(\alpha) = g(\alpha) \cdot h(\alpha) = 0 \cdot h(\alpha) = 0$, the element $\alpha \in \mathcal{O}_K$ is a root of $f$. [/step] [step:Verify $\alpha$ is a simple root of $f$] We show that $f'(\alpha) \neq 0$, which is equivalent to $\alpha$ being a simple root. Since $f(x) = (x - \alpha) \cdot h(x)$, the product rule gives \begin{align*} f'(x) = h(x) + (x - \alpha) h'(x). \end{align*} Evaluating at $x = \alpha$: \begin{align*} f'(\alpha) = h(\alpha). \end{align*} The reduction of $h$ modulo $\mathfrak{m}_K$ satisfies $\bar{h} \equiv \bar{h} \pmod{\mathfrak{m}_K}$ (where we use the same symbol for the original $\bar{h}$ from the coprime factorisation, since Hensel's Lemma guarantees $h$ lifts $\bar{h}$). Evaluating $\bar{h}$ at $\bar{\alpha}$: since $\gcd(x - \bar{\alpha}, \bar{h}) = 1$, we established that $\bar{h}(\bar{\alpha}) \neq 0$. Reducing $h(\alpha)$ modulo $\mathfrak{m}_K$ gives $\bar{h}(\bar{\alpha}) \neq 0$, so $h(\alpha) \notin \mathfrak{m}_K$, which means $|h(\alpha)| = 1$. In particular, $h(\alpha) \neq 0$, so $f'(\alpha) = h(\alpha) \neq 0$, confirming that $\alpha$ is a simple root of $f$. [/step] [step:Prove uniqueness of the lift] Suppose $\alpha' \in \mathcal{O}_K$ is another root of $f$ with $\alpha' \equiv \bar{\alpha} \pmod{\mathfrak{m}_K}$. Since $f(\alpha') = 0$ and $f(x) = (x - \alpha) h(x)$, we have \begin{align*} 0 = f(\alpha') = (\alpha' - \alpha) \cdot h(\alpha'). \end{align*} We claim $h(\alpha') \neq 0$. Reducing modulo $\mathfrak{m}_K$: $\overline{h(\alpha')} = \bar{h}(\bar{\alpha}') = \bar{h}(\bar{\alpha}) \neq 0$ (using $\alpha' \equiv \bar{\alpha} \pmod{\mathfrak{m}_K}$ and the fact established above that $\bar{h}(\bar{\alpha}) \neq 0$). Therefore $h(\alpha') \notin \mathfrak{m}_K$, so $h(\alpha') \neq 0$. Since $\mathcal{O}_K$ is an integral domain (it is a subring of the field $K$), the equation $(\alpha' - \alpha) \cdot h(\alpha') = 0$ with $h(\alpha') \neq 0$ forces $\alpha' - \alpha = 0$, i.e., $\alpha' = \alpha$. [guided] Why must the lift be unique? Suppose two elements $\alpha, \alpha' \in \mathcal{O}_K$ both satisfy $f(\alpha) = f(\alpha') = 0$ and $\alpha \equiv \alpha' \equiv \bar{\alpha} \pmod{\mathfrak{m}_K}$. From the factorisation $f(x) = (x - \alpha) h(x)$, evaluating at $\alpha'$ gives $(\alpha' - \alpha) h(\alpha') = 0$. The key point is that $h(\alpha') \neq 0$: since $\alpha' \equiv \bar{\alpha} \pmod{\mathfrak{m}_K}$, the reduction of $h(\alpha')$ is $\bar{h}(\bar{\alpha})$, which is nonzero because we proved $\gcd(x - \bar{\alpha}, \bar{h}) = 1$. Since $K$ is a field, $\mathcal{O}_K \subset K$ is an integral domain, so the product $(\alpha' - \alpha) h(\alpha') = 0$ with $h(\alpha') \neq 0$ forces $\alpha' = \alpha$. Note that the simplicity hypothesis is essential for uniqueness. If $\bar{\alpha}$ were a multiple root of $\bar{f}$, say of multiplicity $m \geq 2$, then $\bar{h}(\bar{\alpha}) = 0$, and we could not conclude $h(\alpha') \neq 0$. In that case, multiple lifts can exist: for example, $f(x) = x^2 - p$ over $\mathbb{Z}_p$ has the reduction $\bar{f}(x) = x^2$ with $\bar{\alpha} = 0$ a double root. For $p \neq 2$, this polynomial has no root in $\mathbb{Z}_p$ at all (the equation $x^2 = p$ has no solution since $|x|_p^2 = |p|_p = p^{-1}$ would require $|x|_p = p^{-1/2} \notin |K^\times|$). The corollary does not apply because $0$ is not a simple root of $\bar{f}$. [/guided] [/step]