Hensel's lemma on ℤ_p

This file proves Hensel's lemma on ℤ_p, roughly following Keith Conrad's writeup: http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf

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.

References

• http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf
• R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers
• https://en.wikipedia.org/wiki/Hensel%27s_lemma

Tags

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

theorem padic_polynomial_dist {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [CommSemiring R] [Algebra R ℤ_[p]] (F : Polynomial R) (x y : ℤ_[p]) : ‖(Polynomial.aeval x) F - (Polynomial.aeval y) F‖ ≤ ‖x - y‖

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

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