Hensel's lemma on ℤ_p

This file proves Hensel's lemma on ℤ_p, roughly following Keith Conrad's writeup:

Hensel's lemma gives a simple condition for the existence of a root of a polynomial.

The proof and motivation are described in the paper [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019].

References

• [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019]

Tags

p-adic, p adic, padic, p-adic integer

theorem padic_polynomial_dist {p : ℕ} [Fact (Nat.Prime p)] (F : Polynomial ℤ_[p]) (x : ℤ_[p]) (y : ℤ_[p]) : ‖Polynomial.eval x F - Polynomial.eval y F‖ ≤ ‖x - y‖

theorem limit_zero_of_norm_tendsto_zero {p : ℕ} [Fact (Nat.Prime p)] {ncs : CauSeq ℤ_[p] norm} {F : Polynomial ℤ_[p]} (hnorm : Filter.Tendsto (fun (i : ℕ) => ‖Polynomial.eval (↑ncs i) F‖) Filter.atTop (nhds 0)) : Polynomial.eval (CauSeq.lim ncs) F = 0

theorem hensels_lemma {p : ℕ} [Fact (Nat.Prime p)] {F : Polynomial ℤ_[p]} {a : ℤ_[p]} (hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2) : ∃ (z : ℤ_[p]), Polynomial.eval z F = 0 ∧ ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧ ‖Polynomial.eval z (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧ ∀ (z' : ℤ_[p]), Polynomial.eval z' F = 0 → ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ → z' = z