Papers With

← All papers
First page of A formal proof of Hensel's lemma over the p-adic integers

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

Robert Y. Lewis

cs.LO Sep 25, 2019 · v1
formalization mathlib number-theory algebra
Read PDF arXiv abstract
TL;DR
Constructs p-adic numbers in Lean and formally proves a strong form of Hensel's lemma.
Abstract
The field of p-adic numbers and the ring of p-adic integers are essential constructions of modern number theory. Hensel's lemma, described by Gouvea as the most important algebraic property of the p-adic numbers, shows the existence of roots of polynomials over the p-adic integers provided an initial seed point. The theorem can be proved for the p-adics with significantly weaker hypotheses than for general rings. We construct the p-adic numbers and integers 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.
Problem

Hensel's lemma is a central algebraic property of the p-adic numbers, guaranteeing the existence of polynomial roots given an initial approximate root. The p-adic numbers and this result had not been formally verified in a proof assistant.

Approach

The authors construct the field of p-adic numbers and the ring of p-adic integers in the Lean proof assistant, establishing various associated algebraic properties. They then formally prove a strong form of Hensel's lemma, which requires significantly weaker hypotheses for p-adics than for general rings. The proof combines algebraic and analytic reasoning, demonstrating how the Lean mathematical library handles heterogeneous topics.

Results

A strong form of Hensel's lemma over the p-adic integers is formally verified in Lean. The construction includes the p-adic numbers, p-adic integers, and their algebraic properties, demonstrating the integration of algebraic and analytic reasoning in the Lean library.