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