Email Gateway (May 14 2021 at 16:02): 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: Apr 19 2024 at 01:05 UTC