Abstract
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.