mathlib documentation


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].



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