p-adic整数上Hensel引理的一个形式证明
A formal proof of Hensel's lemma over the p-adic integers
摘要：
$p$ -进数域$\mathbb{Q}_p$和$p$ -进整数环$\mathbb{Z}_p$是现代数论的重要构造. Hensel引理被Gouvêa描述为“$p$ -adic数的最重要的代数性质”，证明了在初始种子点的条件下，$\mathbb{Z}_p$上多项式的根的存在性。对于$p$ -自基，该定理可以在比一般环弱得多的假设下得到证明。我们构造$\mathbb{Q}_p$和$\mathbb{Z}_p$在精益证明助手，与各种相关的代数性质，并正式证明强形式的亨塞尔引理。证明是代数和分析推理的交叉点，并演示了精益数学库如何处理这样一个异构的主题。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
