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

less than 1 minute read

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.