English
Hensel's lemma for PadicInt p: under a smallness/derivative-nonvanishing condition, there exists a unique root z ∈ ℤ_p of F with z near a and matching derivative valuations.
Русский
Лемма Хенселя для PadicInt p: при малости \(F(a) \) и ненулевой производной существует единственный корень z ∈ ℤ_p рядом с a, удовлетворяющий условиям по производной.
LaTeX
$$$\exists z ∈ \mathbb{Z}_p : F( z ) = 0 \\ and \\ \|z-a\| < \|F'(a)\|, \; \|F'(z)\| = \|F'(a)\| \\ and \\ (\forall z', F(z')=0 \Rightarrow \|z'-a\| < \|F'(a)\| \Rightarrow z' = z).$$$
Lean4
theorem hensels_lemma :
∃ z : ℤ_[p],
F.aeval z = 0 ∧
‖z - a‖ < ‖F.derivative.aeval a‖ ∧
‖F.derivative.aeval z‖ = ‖F.derivative.aeval a‖ ∧
∀ z', F.aeval z' = 0 → ‖z' - a‖ < ‖F.derivative.aeval a‖ → z' = z :=
by
classical
exact
if ha : F.aeval a = 0 then ⟨a, a_is_soln hnorm ha⟩
else by
exact
⟨soln_gen hnorm, eval_soln hnorm, soln_dist_to_a_lt_deriv hnorm ha, soln_deriv_norm hnorm, fun z =>
soln_unique hnorm ha z⟩
