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

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Padic_Ints

- Function_Ring
- Cring_Poly
- Supplementary_Ring_Facts
- Extended_Int
- Padic_Construction
- Padic_Integers
- Padic_Int_Topology
- Padic_Int_Polynomials
- Hensels_Lemma
- Zp_Compact

### Used by

- p-adic Fields and p-adic Semialgebraic Sets

## Cite

×

Padic_Ints-AFP

    @article{Padic_Ints-AFP,
      author  = {Aaron Crighton},
      title   = {Hensel's Lemma for the p-adic Integers},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Padic_Ints.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- May 14, 2021 : Isabelle2021