# Hensel's lemma on ℤ_p #

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.