p-adic integers #
This file defines the p
-adic integers ℤ_[p]
as the subtype of ℚ_[p]
with norm ≤ 1
.
We show that ℤ_[p]
- is complete,
- is nonarchimedean,
- is a normed ring,
- is a local ring, and
- is a discrete valuation ring.
The relation between ℤ_[p]
and ZMod p
is established in another file.
Important definitions #
PadicInt
: the type ofp
-adic integers
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 [Fact p.Prime]
as a type class argument.
Coercions into ℤ_[p]
are set up to work with the norm_cast
tactic.
References #
- [F. Q. Gouvêa, 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
Ring structure and coercion to ℚ_[p]
#
instance
PadicInt.instNormOneClassPadicIntInstNormPadicIntInstOnePadicInt
(p : ℕ)
[Fact (Nat.Prime p)]
:
Norm #
Valuation on ℤ_[p]
#
PadicInt.valuation
lifts the p
-adic valuation on ℚ
to ℤ_[p]
.
Instances For
@[simp]
@[simp]
@[simp]
theorem
PadicInt.valuation_nonneg
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(x : ℤ_[p])
:
0 ≤ PadicInt.valuation x
@[simp]
theorem
PadicInt.valuation_p_pow_mul
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(n : ℕ)
(c : ℤ_[p])
(hc : c ≠ 0)
:
PadicInt.valuation (↑p ^ n * c) = ↑n + PadicInt.valuation c
Units of ℤ_[p]
#
@[simp]
theorem
PadicInt.unitCoeff_coe
{p : ℕ}
[hp : Fact (Nat.Prime p)]
{x : ℤ_[p]}
(hx : x ≠ 0)
:
↑↑(PadicInt.unitCoeff hx) = ↑x * ↑p ^ (-PadicInt.valuation x)
theorem
PadicInt.unitCoeff_spec
{p : ℕ}
[hp : Fact (Nat.Prime p)]
{x : ℤ_[p]}
(hx : x ≠ 0)
:
x = ↑(PadicInt.unitCoeff hx) * ↑p ^ Int.natAbs (PadicInt.valuation x)
Various characterizations of open unit balls #
theorem
PadicInt.mem_span_pow_iff_le_valuation
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(x : ℤ_[p])
(hx : x ≠ 0)
(n : ℕ)
:
x ∈ Ideal.span {↑p ^ n} ↔ ↑n ≤ PadicInt.valuation x