p-adic Fields and p-adic Semialgebraic Sets

Aaron Crighton

September 22, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Padic_Field