Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Hensel's Lemma for the p-adic ...

view this post on Zulip Email Gateway (May 14 2021 at 16:02):

From: Manuel Eberl <>
Hensel's Lemma for the p-adic Integers

by Aaron Crighton

We formalize the ring of p-adic integers within the framework of the
HOL-Algebra library. The carrier of the ring is formalized as the
inverse limit of quotients of the integers by powers of a fixed prime p.
We define an integer-valued valuation, as well as an extended-integer
valued valuation which sends 0 to the infinite element. Basic
topological facts about the p-adic integers are formalized, including
completeness and sequential compactness. Taylor expansions of
polynomials over a commutative ring are defined, culminating in the
formalization of Hensel's Lemma based on a proof due to Keith Conrad.



Last updated: Dec 08 2021 at 08:24 UTC