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
@[instance]
Addition on ℤ_p is inherited from ℚ_p.
@[instance]
Multiplication on ℤ_p is inherited from ℚ_p.
@[instance]
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, 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 := _}
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
- padic_int.normed_ring = {to_has_norm := padic_int.has_norm _inst_1, to_ring := padic_int.ring _inst_1, to_metric_space := padic_int.metric_space _inst_1, dist_eq := _, norm_mul := _}
@[instance]
def
padic_norm_z.is_absolute_value
{p : ℕ}
[fact (nat.prime p)] :
is_absolute_value (λ (z : ℤ_[p]), ∥z∥)
Equations
- padic_norm_z.is_absolute_value = _
- _ = _
- _ = _
- _ = _
@[instance]
Equations
- padic_int.comm_ring = {add := ring.add padic_int.ring, add_assoc := _, zero := ring.zero padic_int.ring, zero_add := _, add_zero := _, neg := ring.neg padic_int.ring, add_left_neg := _, add_comm := _, mul := ring.mul padic_int.ring, mul_assoc := _, one := ring.one padic_int.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
Equations
- padic_int.integral_domain = {add := comm_ring.add padic_int.comm_ring, add_assoc := _, zero := comm_ring.zero padic_int.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg padic_int.comm_ring, add_left_neg := _, add_comm := _, mul := comm_ring.mul padic_int.comm_ring, mul_assoc := _, one := comm_ring.one padic_int.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
Valuation on ℤ_[p]
Units of ℤ_[p]
unit_coeff hx is the unit u in the unique representation x = u * p ^ n.
See unit_coeff_spec.
@[instance]
Equations
@[instance]
Equations
- padic_int.complete = {is_complete := _}
@[instance]