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 #

Tags #

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

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)) :
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, 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 = 0z' - a < Polynomial.eval a (Polynomial.derivative F)z' = z