mathlib3 documentation

number_theory.padics.hensel

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: http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf

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