p进整数上Hensel引理的形式化证明

$p$进数域 $\mathbb{Q}_p$ 与 $p$进整数环 $\mathbb{Z}_p$ 是现代数论的基本构造。被Gouvêa描述为“$p$进数最重要的代数性质”的Hensel引理，在给定初始种子点的情况下，证明了 $\mathbb{Z}_p$ 上多项式根的存在性。该定理对$p$进数可在比一般环弱得多的假设下被证明。我们在Lean证明辅助器中构造了 $\mathbb{Q}_p$ 和 $\mathbb{Z}_p$ 及其多种相关代数性质，并形式化证明了一种强形式的Hensel引理。该证明位于代数与解析推理的交叉地带，并展示了Lean数学库如何处理此类异质主题。