mathlib3 documentation


Hensel's lemma on ℤ_p #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

References #

Tags #

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