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. 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 p-adic integers ℤ_p are the p-adic numbers with norm ≤ 1.
Instances for padic_int
- padic_int.padic.has_coe
- padic_int.has_add
- padic_int.has_mul
- padic_int.has_neg
- padic_int.has_sub
- padic_int.has_zero
- padic_int.inhabited
- padic_int.has_one
- padic_int.ring
- padic_int.char_zero
- padic_int.metric_space
- padic_int.complete_space
- padic_int.has_norm
- padic_int.normed_comm_ring
- padic_int.norm_one_class
- padic_int.is_domain
- padic_int.complete
- padic_int.local_ring
- padic_int.discrete_valuation_ring
- padic_int.is_adic_complete
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 := _, nsmul := nsmul_rec {add := has_add.add padic_int.has_add}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg padic_int.has_neg, sub := has_sub.sub padic_int.has_sub, sub_eq_add_neg := _, zsmul := zsmul_rec {neg := has_neg.neg padic_int.has_neg}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul padic_int.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul padic_int.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
The inverse of a p-adic integer with norm equal to 1 is also a p-adic integer. Otherwise, the inverse is defined to be 0.
A sequence of integers that is Cauchy with respect to the p
-adic norm
converges to a p
-adic integer.
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 := _}