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.
p-adic, p adic, padic, p-adic integer