A formal proof of Hensel's lemma over the p-adic integers
RY Lewis - Proceedings of the 8th ACM SIGPLAN International …, 2019 - dl.acm.org
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019•dl.acm.org
The field of p-adic numbers ℚ p and the ring of p-adic integers ℤ 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 ℤ 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 ℚ p and ℤ p
in the Lean proof assistant, with various associated algebraic properties, and formally prove …
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 ℤ 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 ℚ p and ℤ p
in the Lean proof assistant, with various associated algebraic properties, and formally prove …
The field of p-adic numbers ℚp and the ring of p-adic integers ℤ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 ℤ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 ℚp and ℤ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.