theorem double_root_iff_derivative_root {R : Type u_1} [CommRing R] (f : Polynomial R) (a : R) : Polynomial.eval a f = 0 ∧ Polynomial.eval a (Polynomial.derivative f) = 0 ↔ (Polynomial.X - Polynomial.C a) ^ 2 ∣ f

Lemma 8.7: over any commutative ring $R$, an element $a \in R$ is a double root of $f \in R[X]$ (i.e. $f(a) = 0$ and $f'(a) = 0$) if and only if $(X-a)^2$ divides $f$.

@[reducible, inline]

noncomputable abbrev formalDerivative {R : Type u_1} [CommSemiring R] (f : Polynomial R) : Polynomial R

Definition 8.6 (formal derivative): for a polynomial $f \in R[X]$ over a commutative semiring, the formal derivative $f'$ is the polynomial obtained term-by-term. Thin abbreviation for Polynomial.derivative.

theorem PadicInt.norm_eq_one_of_not_dvd {p : ℕ} [Fact (Nat.Prime p)] (x : ℤ_[p]) (h : ¬↑p ∣ x) : ‖x‖ = 1

If $x \in \mathbb{Z}_p$ is not divisible by $p$, then $\|x\| = 1$. Equivalently, $x$ is a unit in $\mathbb{Z}_p$.

theorem hensel_lemma {p : ℕ} [Fact (Nat.Prime p)] (f : Polynomial ℤ_[p]) (a : ℤ_[p]) (hfa : ↑p ∣ (Polynomial.aeval a) f) (hda : ¬↑p ∣ (Polynomial.aeval a) (Polynomial.derivative f)) : ∃! b : ℤ_[p], (Polynomial.aeval b) f = 0 ∧ ↑p ∣ b - a

Theorem 8.8 (Hensel's lemma, divisibility form): given $f \in \mathbb{Z}_p[X]$ and $a \in \mathbb{Z}_p$ with $p \mid f(a)$ and $p \nmid f'(a)$, there exists a unique $b \in \mathbb{Z}_p$ with $f(b) = 0$ and $p \mid (b - a)$.

theorem hensel_lemma_norm {p : ℕ} [Fact (Nat.Prime p)] (f : Polynomial ℤ_[p]) (a : ℤ_[p]) (hfa : ‖(Polynomial.aeval a) f‖ < 1) (hda : ‖(Polynomial.aeval a) (Polynomial.derivative f)‖ = 1) : ∃! b : ℤ_[p], (Polynomial.aeval b) f = 0 ∧ ‖b - a‖ < 1

Theorem 8.8 (Hensel's lemma, norm form): given $f \in \mathbb{Z}_p[X]$ and $a \in \mathbb{Z}_p$ with $\|f(a)\| < 1$ and $\|f'(a)\| = 1$, there exists a unique $b \in \mathbb{Z}_p$ with $f(b) = 0$ and $\|b - a\| < 1$.