Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Hensel's Lemma for the p-adic ...


view this post on Zulip Email Gateway (May 14 2021 at 16:02):

From: Manuel Eberl <eberlm@in.tum.de>
Hensel's Lemma for the p-adic Integers

by Aaron Crighton

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.

https://www.isa-afp.org/entries/Padic_Ints.html

Enjoy

Manuel
smime.p7s


Last updated: Dec 08 2021 at 08:24 UTC