p-adic integers

This file defines the p-adic integers ℤ_p as the subtype of ℚ_p with norm ≤ 1. We show that ℤ_p is a complete nonarchimedean normed local ring.

Important definitions

• padic_int : the type of p-adic numbers

Notation

We introduce the notation ℤ_[p] for the p-adic integers.

Implementation notes

Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically by taking (prime p) as a type class argument.

Coercions into ℤ_p are set up to work with the norm_cast tactic.

References

• [F. Q. Gouêva, p-adic numbers][gouvea1997]
• [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019]
• https://en.wikipedia.org/wiki/P-adic_number

Tags

p-adic, p adic, padic, p-adic integer