### Abstract

The field of p-adic numbers for a prime integer p is constructed. Basic facts about p-adic topology including Hensel's Lemma are proved, building on a prior submission by the author. The theory of semialgebraic sets and semialgebraic functions on cartesian powers of p-adic fields is also developed, following a formalization of these concepts due to Denef. This is done towards a formalization of Denef's proof of Macintyre's quantifier elimination theorem for p-adic fields. Theories developing general multivariable polynomial rings over a commutative ring are developed, as well as some general theory of cartesian powers of an arbitrary ring.

### License

BSD License

### Topics

- Mathematics/Number theory
- Mathematics/Algebra

### Session Padic_Field

- Fraction_Field
- Cring_Multivariable_Poly
- Indices
- Ring_Powers
- Padic_Fields
- Padic_Field_Polynomials
- Padic_Field_Topology
- Generated_Boolean_Algebra
- Padic_Field_Powers
- Padic_Semialgebraic_Function_Ring

### Depends on

- The Localization of a Commutative Ring
- Hensel’s Lemma for the p-adic Integers

### Auto-related entries

- Diophantine Equations and the DPRM Theorem

## Cite

×

Padic_Field-AFP

    @article{Padic_Field-AFP,
      author  = {Aaron Crighton},
      title   = {p-adic Fields and p-adic Semialgebraic Sets},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Padic_Field.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Sep 22, 2022 : Isabelle2021-1