Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: p-Adic Fields and p-Adic Semia...


view this post on Zulip Email Gateway (Sep 22 2022 at 16:35):

From: Manuel Eberl <manuel@pruvisto.org>
After an awfully, if not to say embarrassingly long processing time –
due to both the rather large size of the entry and some technical
problems – I can finally present to you the following entry, which
boasts a staggering 40000 lines:

p-Adic Fields and p-Adic Semialgebraic Sets

by Aaron Crighton

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.

Enjoy,

Manuel


Last updated: Mar 29 2024 at 04:18 UTC