### Abstract

We formalize the ring of

BSD License*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.