# A formal proof of Hensel’s lemma over the p-adic integers

** Published:**

Here you will find the supplementary materials to my paper *A formal proof of Hensel’s lemma over the p-adic integers*. This paper was published at CPP 2019. For more information, contact Robert Y. Lewis.

### The Formal Development

The project described in the linked paper has been incorporated into the Lean mathlib repository. The current state of the p-adic number development can be found in the directory /data/padics/. See also the pull requests here and here.

Since mathlib is regularly updated, we preserve a branch here that shows its state when this paper was written.