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
- R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers
- https://en.wikipedia.org/wiki/P-adic_number
Tags #
p-adic, p adic, padic, p-adic integer
The ring of p
-adic integers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Ring structure and coercion to ℚ_[p]
#
Equations
- PadicInt.instAddCommGroup = inferInstance
Alias of PadicInt.coe_natCast
.
Alias of PadicInt.coe_intCast
.
A sequence of integers that is Cauchy with respect to the p
-adic norm converges to a p
-adic
integer.
Equations
- PadicInt.ofIntSeq seq h = ⟨⟦⟨fun (n : ℕ) => ↑(seq n), h⟩⟧, ⋯⟩
Instances For
Equations
- PadicInt.instMetricSpace p = Subtype.metricSpace
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
Equations
- ⋯ = ⋯
Norm #
Equations
- ⋯ = ⋯
Valuation on ℤ_[p]
#
PadicInt.valuation
lifts the p
-adic valuation on ℚ
to ℤ_[p]
.
Equations
- x.valuation = (↑x).valuation
Instances For
Units of ℤ_[p]
#
unitCoeff hx
is the unit u
in the unique representation x = u * p ^ n
.
See unitCoeff_spec
.
Equations
Instances For
Various characterizations of open unit balls #
Discrete valuation ring #
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- PadicInt.algebra = Algebra.ofSubring (PadicInt.subring p)