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

Abstract

The field of $p$-adic numbers ${\mathbb{Q}}_p$ and the ring of $p$-adic integers ${\mathbb{Z}}_p$ are essential constructions of modern number theory. Hensel's lemma, described by Gouvêa as the "most important algebraic property of the $p$-adic numbers," shows the existence of roots of polynomials over ${\mathbb{Z}}_p$ provided an initial seed point. The theorem can be proved for the $p$-adics with significantly weaker hypotheses than for general rings. We construct ${\mathbb{Q}}_p$ and ${\mathbb{Z}}_p$ in the Lean proof assistant, with various associated algebraic properties, and formally prove a strong form of Hensel's lemma. The proof lies at the intersection of algebraic and analytic reasoning and demonstrates how the Lean mathematical library handles such a heterogeneous topic.

CPP 2019

References in corpus (3)

• A formal proof of the four color theorem
• An Extensible Ad Hoc Interface between Lean and Mathematica
• Formalization of the prime number theorem and Dirichlet's theorem

Cited by in corpus (4)

• The Lean mathematical library
• Formalizing the Ring of Witt Vectors
• Formalizing the Solution to the Cap Set Problem
• On the relation between perfect powers and tetration frozen digits