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
- is a discrete valuation ring
The relation between ℤ_[p]
and zmod p
is established in another file.
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 `[fact (nat.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
Ring structure and coercion to ℚ_[p]
Addition on ℤ_p is inherited from ℚ_p.
Multiplication on ℤ_p is inherited from ℚ_p.
Subtraction on ℤ_p is inherited from ℚ_p.
Equations
- padic_int.ring = {add := has_add.add padic_int.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg padic_int.has_neg, sub := has_sub.sub padic_int.has_sub, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := has_mul.mul padic_int.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
A sequence of integers that is Cauchy with respect to the p
-adic norm
converges to a p
-adic integer.
Instances
We now show that ℤ_[p]
is a
- complete metric space
- normed ring
- integral domain
Equations
Equations
- padic_int.normed_comm_ring p = {to_normed_ring := {to_has_norm := padic_int.has_norm p _inst_1, to_ring := padic_int.ring _inst_1, to_metric_space := padic_int.metric_space p _inst_1, dist_eq := _, norm_mul := _}, mul_comm := _}
Equations
- padic_int.integral_domain = {add := ring.add normed_ring.to_ring, add_assoc := _, zero := ring.zero normed_ring.to_ring, zero_add := _, add_zero := _, neg := ring.neg normed_ring.to_ring, sub := ring.sub normed_ring.to_ring, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul normed_ring.to_ring, mul_assoc := _, one := ring.one normed_ring.to_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
Norm
Equations
- padic_int.complete p = {is_complete := _}