# mathlibdocumentation

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.

## Tags #

def padic_int (p : ) [fact (nat.prime p)] :
Type

The p-adic integers ℤ_p are the p-adic numbers with norm ≤ 1.

Equations

### Ring structure and coercion to ℚ_[p]#

@[protected, instance]
Equations
theorem padic_int.ext {p : } [fact (nat.prime p)] {x y : ℤ_[p]} :
x = yx = y
@[protected, instance]

Addition on ℤ_p is inherited from ℚ_p.

Equations
@[protected, instance]
def padic_int.has_mul {p : } [fact (nat.prime p)] :

Multiplication on ℤ_p is inherited from ℚ_p.

Equations
• padic_int.has_mul._match_2 x, hx⟩ = λ (_x : ℤ_[p]), padic_int.has_mul._match_1 x hx _x
• padic_int.has_mul._match_1 x hx y, hy⟩ = x * y, _⟩
@[protected, instance]
def padic_int.has_neg {p : } [fact (nat.prime p)] :

Negation on ℤ_p is inherited from ℚ_p.

Equations
@[protected, instance]
def padic_int.has_sub {p : } [fact (nat.prime p)] :

Subtraction on ℤ_p is inherited from ℚ_p.

Equations
• padic_int.has_sub._match_2 x, hx⟩ = λ (_x : ℤ_[p]), padic_int.has_sub._match_1 x hx _x
• padic_int.has_sub._match_1 x hx y, hy⟩ = x - y, _⟩
@[protected, instance]
def padic_int.has_zero {p : } [fact (nat.prime p)] :

Zero on ℤ_p is inherited from ℚ_p.

Equations
@[protected, instance]
def padic_int.inhabited {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
def padic_int.has_one {p : } [fact (nat.prime p)] :

One on ℤ_p is inherited from ℚ_p.

Equations
@[simp]
theorem padic_int.mk_zero {p : } [fact (nat.prime p)] {h : 0 1} :
0, h⟩ = 0
@[simp]
theorem padic_int.val_eq_coe {p : } [fact (nat.prime p)] (z : ℤ_[p]) :
z.val = z
@[simp, norm_cast]
theorem padic_int.coe_add {p : } [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :
(z1 + z2) = z1 + z2
@[simp, norm_cast]
theorem padic_int.coe_mul {p : } [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :
z1 * z2 = (z1) * z2
@[simp, norm_cast]
theorem padic_int.coe_neg {p : } [fact (nat.prime p)] (z1 : ℤ_[p]) :
-z1 = -z1
@[simp, norm_cast]
theorem padic_int.coe_sub {p : } [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :
(z1 - z2) = z1 - z2
@[simp, norm_cast]
theorem padic_int.coe_one {p : } [fact (nat.prime p)] :
1 = 1
@[simp, norm_cast]
theorem padic_int.coe_coe {p : } [fact (nat.prime p)] (n : ) :
@[simp, norm_cast]
theorem padic_int.coe_coe_int {p : } [fact (nat.prime p)] (z : ) :
@[simp, norm_cast]
theorem padic_int.coe_zero {p : } [fact (nat.prime p)] :
0 = 0
@[protected, instance]
def padic_int.ring {p : } [fact (nat.prime p)] :
Equations

The coercion from ℤ[p] to ℚ[p] as a ring homomorphism.

Equations
@[simp, norm_cast]
theorem padic_int.coe_pow {p : } [fact (nat.prime p)] (x : ℤ_[p]) (n : ) :
(x ^ n) = x ^ n
@[simp]
theorem padic_int.mk_coe {p : } [fact (nat.prime p)] (k : ℤ_[p]) :
k, _⟩ = k
def padic_int.inv {p : } [fact (nat.prime p)] :

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.

Equations
@[protected, instance]
def padic_int.char_zero {p : } [fact (nat.prime p)] :
@[simp, norm_cast]
theorem padic_int.coe_int_eq {p : } [fact (nat.prime p)] (z1 z2 : ) :
z1 = z2 z1 = z2
def padic_int.of_int_seq {p : } [fact (nat.prime p)] (seq : ) (h : (λ (n : ), (seq n))) :

A sequence of integers that is Cauchy with respect to the p-adic norm converges to a p-adic integer.

Equations

### Instances #

We now show that ℤ_[p] is a

• complete metric space
• normed ring
• integral domain
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def padic_int.has_norm (p : ) [fact (nat.prime p)] :
Equations
@[protected]
theorem padic_int.mul_comm {p : } [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :
z1 * z2 = z2 * z1
@[protected]
theorem padic_int.zero_ne_one {p : } [fact (nat.prime p)] :
0 1
@[protected]
theorem padic_int.eq_zero_or_eq_zero_of_mul_eq_zero {p : } [fact (nat.prime p)] (a b : ℤ_[p]) :
a * b = 0a = 0 b = 0
theorem padic_int.norm_def {p : } [fact (nat.prime p)] {z : ℤ_[p]} :
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations

### Norm #

theorem padic_int.norm_le_one {p : } [fact (nat.prime p)] (z : ℤ_[p]) :
@[simp]
theorem padic_int.norm_mul {p : } [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :
z1 * z2 = z1 * z2
@[simp]
theorem padic_int.norm_pow {p : } [fact (nat.prime p)] (z : ℤ_[p]) (n : ) :
z ^ n = z ^ n
theorem padic_int.nonarchimedean {p : } [fact (nat.prime p)] (q r : ℤ_[p]) :
theorem padic_int.norm_eq_of_norm_add_lt_right {p : } [fact (nat.prime p)] {z1 z2 : ℤ_[p]} (h : z1 + z2 < z2) :
theorem padic_int.norm_eq_of_norm_add_lt_left {p : } [fact (nat.prime p)] {z1 z2 : ℤ_[p]} (h : z1 + z2 < z1) :
@[simp]
theorem padic_int.norm_eq_padic_norm {p : } [fact (nat.prime p)] {q : ℚ_[p]} (hq : q 1) :
q, hq⟩ = q
@[simp]
theorem padic_int.norm_p {p : } [fact (nat.prime p)] :
@[simp]
theorem padic_int.norm_p_pow {p : } [fact (nat.prime p)] (n : ) :
@[protected, instance]
def padic_int.complete (p : ) [fact (nat.prime p)] :
Equations
theorem padic_int.exists_pow_neg_lt (p : ) [hp_prime : fact (nat.prime p)] {ε : } (hε : 0 < ε) :
∃ (k : ), p ^ -k < ε
theorem padic_int.exists_pow_neg_lt_rat (p : ) [hp_prime : fact (nat.prime p)] {ε : } (hε : 0 < ε) :
∃ (k : ), p ^ -k < ε
theorem padic_int.norm_int_lt_one_iff_dvd {p : } [hp_prime : fact (nat.prime p)] (k : ) :
theorem padic_int.norm_int_le_pow_iff_dvd {p : } [hp_prime : fact (nat.prime p)] {k : } {n : } :

### Valuation on ℤ_[p]#

def padic_int.valuation {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :

padic_int.valuation lifts the p-adic valuation on ℚ to ℤ_[p].

Equations
theorem padic_int.norm_eq_pow_val {p : } [hp_prime : fact (nat.prime p)] {x : ℤ_[p]} (hx : x 0) :
@[simp]
theorem padic_int.valuation_zero {p : } [hp_prime : fact (nat.prime p)] :
@[simp]
theorem padic_int.valuation_one {p : } [hp_prime : fact (nat.prime p)] :
@[simp]
theorem padic_int.valuation_p {p : } [hp_prime : fact (nat.prime p)] :
theorem padic_int.valuation_nonneg {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :
@[simp]
theorem padic_int.valuation_p_pow_mul {p : } [hp_prime : fact (nat.prime p)] (n : ) (c : ℤ_[p]) (hc : c 0) :
((p ^ n) * c).valuation = n + c.valuation

### Units of ℤ_[p]#

theorem padic_int.mul_inv {p : } [hp_prime : fact (nat.prime p)] {z : ℤ_[p]} :
z = 1z * z.inv = 1
theorem padic_int.inv_mul {p : } [hp_prime : fact (nat.prime p)] {z : ℤ_[p]} (hz : z = 1) :
(z.inv) * z = 1
theorem padic_int.is_unit_iff {p : } [hp_prime : fact (nat.prime p)] {z : ℤ_[p]} :
theorem padic_int.norm_lt_one_add {p : } [hp_prime : fact (nat.prime p)] {z1 z2 : ℤ_[p]} (hz1 : z1 < 1) (hz2 : z2 < 1) :
z1 + z2 < 1
theorem padic_int.norm_lt_one_mul {p : } [hp_prime : fact (nat.prime p)] {z1 z2 : ℤ_[p]} (hz2 : z2 < 1) :
z1 * z2 < 1
@[simp]
theorem padic_int.mem_nonunits {p : } [hp_prime : fact (nat.prime p)] {z : ℤ_[p]} :
def padic_int.mk_units {p : } [hp_prime : fact (nat.prime p)] {u : ℚ_[p]} (h : u = 1) :

A p-adic number u with ∥u∥ = 1 is a unit of ℤ_[p].

Equations
@[simp]
theorem padic_int.mk_units_eq {p : } [hp_prime : fact (nat.prime p)] {u : ℚ_[p]} (h : u = 1) :
@[simp]
theorem padic_int.norm_units {p : } [hp_prime : fact (nat.prime p)] (u : units ℤ_[p]) :
def padic_int.unit_coeff {p : } [hp_prime : fact (nat.prime p)] {x : ℤ_[p]} (hx : x 0) :

unit_coeff hx is the unit u in the unique representation x = u * p ^ n. See unit_coeff_spec`.

Equations
@[simp]
theorem padic_int.unit_coeff_coe {p : } [hp_prime : fact (nat.prime p)] {x : ℤ_[p]} (hx : x 0) :
theorem padic_int.unit_coeff_spec {p : } [hp_prime : fact (nat.prime p)] {x : ℤ_[p]} (hx : x 0) :

### Various characterizations of open unit balls #

theorem padic_int.norm_le_pow_iff_le_valuation {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (hx : x 0) (n : ) :
theorem padic_int.mem_span_pow_iff_le_valuation {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (hx : x 0) (n : ) :
theorem padic_int.norm_le_pow_iff_mem_span_pow {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (n : ) :
theorem padic_int.norm_le_pow_iff_norm_lt_pow_add_one {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (n : ) :
x p ^ n x < p ^ (n + 1)
theorem padic_int.norm_lt_pow_iff_norm_le_pow_sub_one {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (n : ) :
x < p ^ n x p ^ (n - 1)
theorem padic_int.norm_lt_one_iff_dvd {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :
@[simp]
theorem padic_int.pow_p_dvd_int_iff {p : } [hp_prime : fact (nat.prime p)] (n : ) (a : ) :
p ^ n a p ^ n a

### Discrete valuation ring #

@[protected, instance]
def padic_int.local_ring {p : } [hp_prime : fact (nat.prime p)] :
theorem padic_int.p_nonnunit {p : } [hp_prime : fact (nat.prime p)] :
theorem padic_int.maximal_ideal_eq_span_p {p : } [hp_prime : fact (nat.prime p)] :
theorem padic_int.prime_p {p : } [hp_prime : fact (nat.prime p)] :
theorem padic_int.irreducible_p {p : } [hp_prime : fact (nat.prime p)] :
@[protected, instance]
def padic_int.discrete_valuation_ring {p : } [hp_prime : fact (nat.prime p)] :
theorem padic_int.ideal_eq_span_pow_p {p : } [hp_prime : fact (nat.prime p)] {s : ideal ℤ_[p]} (hs : s ) :
∃ (n : ), s = ideal.span {p ^ n}