Email Gateway (Jul 07 2025 at 08:15): Email Gateway (Jul 07 2025 at 08:15):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’m happy to announce a new AFP entry.
Computational p-Adics
by Jeremy Sylvestre
Abstract
We develop a framework for reasoning computationally about p-adic fields via
formal Laurent series with integer coefficients. We define a ring-class quotient
type consisting of equivalence classes of prime-indexed sequences of formal
Laurent series, in which every p-adic field is contained as a subring. Via a
further quotient of the ring of p-adic integers (that is, the elements of depth
at least 0) by the prime ideal (that is, the subring of elements of depth at
least 1), we define a ring-class type in which every prime-order finite field is
contained as a subring. Finally, some topological properties are developed using
depth as a proxy for a metric, Hensel's Lemma is proved, and the compactness of
local rings of integers is established.
https://www.isa-afp.org/entries/Computational_pAdics.html
Enjoy,
René
Last updated: Jul 26 2025 at 12:43 UTC