# mathlib3documentation

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the p-adic numbers (rationals) ℚ_[p] as the completion of ℚ with respect to the p-adic norm. We show that the p-adic norm on ℚ extends to ℚ_[p], that ℚ is embedded in ℚ_[p], and that ℚ_[p] is Cauchy complete.

## Important definitions #

• padic : the type of p-adic numbers
• padic_norm_e : the rational valued p-adic norm on ℚ_[p]
• padic.add_valuation : the additive p-adic valuation on ℚ_[p], with values in with_top ℤ

## Notation #

We introduce the notation ℚ_[p] for the p-adic numbers.

## 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.

We use the same concrete Cauchy sequence construction that is used to construct ℝ. ℚ_[p] inherits a field structure from this construction. The extension of the norm on ℚ to ℚ_[p] is not analogous to extending the absolute value to ℝ and hence the proof that ℚ_[p] is complete is different from the proof that ℝ is complete.

A small special-purpose simplification tactic, padic_index_simp, is used to manipulate sequence indices in the proof that the norm extends.

padic_norm_e is the rational-valued p-adic norm on ℚ_[p]. To instantiate ℚ_[p] as a normed field, we must cast this into a ℝ-valued norm. The ℝ-valued norm, using notation ‖ ‖ from normed spaces, is the canonical representation of this norm.

simp prefers padic_norm to padic_norm_e when possible. Since padic_norm_e and ‖ ‖ have different types, simp does not rewrite one to the other.

Coercions from ℚ to ℚ_[p] are set up to work with the norm_cast tactic.

## Tags #

@[reducible]
def padic_seq (p : ) :

The type of Cauchy sequences of rationals with respect to the p-adic norm.

Equations
theorem padic_seq.stationary {p : } [fact (nat.prime p)] {f : (padic_norm p)} (hf : ¬f 0) :
(N : ), (m n : ), N m N n (f n) = (f m)

The p-adic norm of the entries of a nonzero Cauchy sequence of rationals is eventually constant.

noncomputable def padic_seq.stationary_point {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) :

For all n ≥ stationary_point f hf, the p-adic norm of f n is the same.

Equations
theorem padic_seq.stationary_point_spec {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) {m n : } :
(f n) = (f m)
noncomputable def padic_seq.norm {p : } [fact (nat.prime p)] (f : padic_seq p) :

Since the norm of the entries of a Cauchy sequence is eventually stationary, we can lift the norm to sequences.

Equations
theorem padic_seq.norm_zero_iff {p : } [fact (nat.prime p)] (f : padic_seq p) :
f.norm = 0 f 0
theorem padic_seq.equiv_zero_of_val_eq_of_equiv_zero {p : } [fact (nat.prime p)] {f g : padic_seq p} (h : (k : ), (f k) = (g k)) (hf : f 0) :
g 0
theorem padic_seq.norm_nonzero_of_not_equiv_zero {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) :
f.norm 0
theorem padic_seq.norm_eq_norm_app_of_nonzero {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) :
(k : ), f.norm = k k 0
theorem padic_seq.not_lim_zero_const_of_nonzero {p : } [fact (nat.prime p)] {q : } (hq : q 0) :
theorem padic_seq.not_equiv_zero_const_of_nonzero {p : } [fact (nat.prime p)] {q : } (hq : q 0) :
¬ q 0
theorem padic_seq.norm_nonneg {p : } [fact (nat.prime p)] (f : padic_seq p) :
0 f.norm
theorem padic_seq.lift_index_left_left {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) (v2 v3 : ) :
(f = (f v3)))

An auxiliary lemma for manipulating sequence indices.

theorem padic_seq.lift_index_left {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) (v1 v3 : ) :
(f = (f v3)))

An auxiliary lemma for manipulating sequence indices.

theorem padic_seq.lift_index_right {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) (v1 v2 : ) :

An auxiliary lemma for manipulating sequence indices.

### Valuation on padic_seq#

noncomputable def padic_seq.valuation {p : } [fact (nat.prime p)] (f : padic_seq p) :

The p-adic valuation on ℚ lifts to padic_seq p. valuation f is defined to be the valuation of the (ℚ-valued) stationary point of f.

Equations
theorem padic_seq.norm_eq_pow_val {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) :
theorem padic_seq.val_eq_iff_norm_eq {p : } [fact (nat.prime p)] {f g : padic_seq p} (hf : ¬f 0) (hg : ¬g 0) :
f.norm = g.norm

This is a special-purpose tactic that lifts padic_norm (f (stationary_point f)) to padic_norm (f (max _ _ _)).

theorem padic_seq.norm_mul {p : } [hp : fact (nat.prime p)] (f g : padic_seq p) :
(f * g).norm = f.norm * g.norm
theorem padic_seq.eq_zero_iff_equiv_zero {p : } [hp : fact (nat.prime p)] (f : padic_seq p) :
f 0
theorem padic_seq.ne_zero_iff_nequiv_zero {p : } [hp : fact (nat.prime p)] (f : padic_seq p) :
¬f 0
theorem padic_seq.norm_const {p : } [hp : fact (nat.prime p)] (q : ) :
= q
theorem padic_seq.norm_values_discrete {p : } [hp : fact (nat.prime p)] (a : padic_seq p) (ha : ¬a 0) :
(z : ), a.norm = p ^ -z
theorem padic_seq.norm_one {p : } [hp : fact (nat.prime p)] :
1.norm = 1
theorem padic_seq.norm_equiv {p : } [hp : fact (nat.prime p)] {f g : padic_seq p} (hfg : f g) :
f.norm = g.norm
theorem padic_seq.norm_nonarchimedean {p : } [hp : fact (nat.prime p)] (f g : padic_seq p) :
(f + g).norm
theorem padic_seq.norm_eq {p : } [hp : fact (nat.prime p)] {f g : padic_seq p} (h : (k : ), (f k) = (g k)) :
f.norm = g.norm
theorem padic_seq.norm_neg {p : } [hp : fact (nat.prime p)] (a : padic_seq p) :
(-a).norm = a.norm
theorem padic_seq.norm_eq_of_add_equiv_zero {p : } [hp : fact (nat.prime p)] {f g : padic_seq p} (h : f + g 0) :
f.norm = g.norm
theorem padic_seq.add_eq_max_of_ne {p : } [hp : fact (nat.prime p)] {f g : padic_seq p} (hfgne : f.norm g.norm) :
(f + g).norm =
def padic (p : ) [fact (nat.prime p)] :

The p-adic numbers ℚ_[p] are the Cauchy completion of ℚ with respect to the p-adic norm.

Equations
Instances for padic
@[protected, instance]
noncomputable def padic.field {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
noncomputable def padic.inhabited {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
def padic.comm_ring {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
def padic.ring {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
def padic.has_zero {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
def padic.has_one {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def padic.has_mul {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
def padic.has_sub {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
def padic.has_neg {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
noncomputable def padic.has_div {p : } [fact (nat.prime p)] :
Equations
@[protected, instance]
Equations
def padic.mk {p : } [fact (nat.prime p)] :

Builds the equivalence class of a Cauchy sequence of rationals.

Equations
theorem padic.zero_def (p : ) [fact (nat.prime p)] :
theorem padic.mk_eq (p : ) [fact (nat.prime p)] {f g : padic_seq p} :
f g
theorem padic.const_equiv (p : ) [fact (nat.prime p)] {q r : } :
q r q = r
@[norm_cast]
theorem padic.coe_inj (p : ) [fact (nat.prime p)] {q r : } :
q = r q = r
@[protected, instance]
def padic.char_zero (p : ) [fact (nat.prime p)] :
@[norm_cast]
theorem padic.coe_add (p : ) [fact (nat.prime p)] {x y : } :
(x + y) = x + y
@[norm_cast]
theorem padic.coe_neg (p : ) [fact (nat.prime p)] {x : } :
@[norm_cast]
theorem padic.coe_mul (p : ) [fact (nat.prime p)] {x y : } :
(x * y) = x * y
@[norm_cast]
theorem padic.coe_sub (p : ) [fact (nat.prime p)] {x y : } :
(x - y) = x - y
@[norm_cast]
theorem padic.coe_div (p : ) [fact (nat.prime p)] {x y : } :
(x / y) = x / y
@[norm_cast]
theorem padic.coe_one (p : ) [fact (nat.prime p)] :
1 = 1
@[norm_cast]
theorem padic.coe_zero (p : ) [fact (nat.prime p)] :
0 = 0
noncomputable def padic_norm_e {p : } [hp : fact (nat.prime p)] :

The rational-valued p-adic norm on ℚ_[p] is lifted from the norm on Cauchy sequences. The canonical form of this function is the normed space instance, with notation ‖ ‖.

Equations
theorem padic_norm_e.defn {p : } [fact (nat.prime p)] (f : padic_seq p) {ε : } (hε : 0 < ε) :
(N : ), (i : ), i N padic_norm_e (f - (f i)) < ε
theorem padic_norm_e.nonarchimedean' {p : } [fact (nat.prime p)] (q r : ℚ_[p]) :

Theorems about padic_norm_e are named with a ' so the names do not conflict with the equivalent theorems about norm (‖ ‖).

theorem padic_norm_e.add_eq_max_of_ne' {p : } [fact (nat.prime p)] {q r : ℚ_[p]} :

Theorems about padic_norm_e are named with a ' so the names do not conflict with the equivalent theorems about norm (‖ ‖).

@[simp]
theorem padic_norm_e.eq_padic_norm' {p : } [fact (nat.prime p)] (q : ) :
@[protected]
theorem padic_norm_e.image' {p : } [fact (nat.prime p)] {q : ℚ_[p]} :
q 0 ( (n : ), = p ^ -n)
theorem padic.rat_dense' {p : } [fact (nat.prime p)] (q : ℚ_[p]) {ε : } (hε : 0 < ε) :
(r : ), padic_norm_e (q - r) < ε
noncomputable def padic.lim_seq {p : } [fact (nat.prime p)] (f : padic_norm_e) :

lim_seq f, for f a Cauchy sequence of p-adic numbers, is a sequence of rationals with the same limit point as f.

Equations
theorem padic.exi_rat_seq_conv {p : } [fact (nat.prime p)] (f : padic_norm_e) {ε : } (hε : 0 < ε) :
(N : ), (i : ), i N padic_norm_e (f i - i)) < ε
theorem padic.complete' {p : } [fact (nat.prime p)] (f : padic_norm_e) :
(q : ℚ_[p]), (ε : ), ε > 0 ( (N : ), (i : ), i N padic_norm_e (q - f i) < ε)
@[protected, instance]
noncomputable def padic.has_dist (p : ) [fact (nat.prime p)] :
Equations
@[protected, instance]
noncomputable def padic.metric_space (p : ) [fact (nat.prime p)] :
Equations
@[protected, instance]
noncomputable def padic.has_norm (p : ) [fact (nat.prime p)] :
Equations
@[protected, instance]
noncomputable def padic.normed_field (p : ) [fact (nat.prime p)] :
Equations
@[protected, instance]
theorem padic.rat_dense (p : ) [fact (nat.prime p)] (q : ℚ_[p]) {ε : } (hε : 0 < ε) :
(r : ), q - r < ε
@[protected, simp]
theorem padic_norm_e.mul {p : } [hp : fact (nat.prime p)] (q r : ℚ_[p]) :
@[protected]
theorem padic_norm_e.is_norm {p : } [hp : fact (nat.prime p)] (q : ℚ_[p]) :
theorem padic_norm_e.nonarchimedean {p : } [hp : fact (nat.prime p)] (q r : ℚ_[p]) :
theorem padic_norm_e.add_eq_max_of_ne {p : } [hp : fact (nat.prime p)] {q r : ℚ_[p]} (h : q r) :
q + r =
@[simp]
theorem padic_norm_e.eq_padic_norm {p : } [hp : fact (nat.prime p)] (q : ) :
@[simp]
theorem padic_norm_e.norm_p {p : } [hp : fact (nat.prime p)] :
theorem padic_norm_e.norm_p_lt_one {p : } [hp : fact (nat.prime p)] :
@[simp]
theorem padic_norm_e.norm_p_zpow {p : } [hp : fact (nat.prime p)] (n : ) :
@[simp]
theorem padic_norm_e.norm_p_pow {p : } [hp : fact (nat.prime p)] (n : ) :
@[protected, instance]
noncomputable def padic_norm_e.padic.nontrivially_normed_field {p : } [hp : fact (nat.prime p)] :
Equations
@[protected]
theorem padic_norm_e.image {p : } [hp : fact (nat.prime p)] {q : ℚ_[p]} :
q 0 ( (n : ), q = (p ^ -n))
@[protected]
theorem padic_norm_e.is_rat {p : } [hp : fact (nat.prime p)] (q : ℚ_[p]) :
(q' : ), q = q'
noncomputable def padic_norm_e.rat_norm {p : } [hp : fact (nat.prime p)] (q : ℚ_[p]) :

rat_norm q, for a p-adic number q is the p-adic norm of q, as rational number.

The lemma padic_norm_e.eq_rat_norm asserts ‖q‖ = rat_norm q.

Equations
theorem padic_norm_e.eq_rat_norm {p : } [hp : fact (nat.prime p)] (q : ℚ_[p]) :
theorem padic_norm_e.norm_rat_le_one {p : } [hp : fact (nat.prime p)] {q : } (hq : ¬p q.denom) :
theorem padic_norm_e.norm_int_le_one {p : } [hp : fact (nat.prime p)] (z : ) :
theorem padic_norm_e.norm_int_le_pow_iff_dvd {p : } [hp : fact (nat.prime p)] (k : ) (n : ) :
theorem padic_norm_e.eq_of_norm_add_lt_right {p : } [hp : fact (nat.prime p)] {z1 z2 : ℚ_[p]} (h : z1 + z2 < z2) :
theorem padic_norm_e.eq_of_norm_add_lt_left {p : } [hp : fact (nat.prime p)] {z1 z2 : ℚ_[p]} (h : z1 + z2 < z1) :
@[protected, instance]
def padic.complete {p : } [hp : fact (nat.prime p)] :
theorem padic.padic_norm_e_lim_le {p : } [hp : fact (nat.prime p)] {f : has_norm.norm} {a : } (ha : 0 < a) (hf : (i : ), f i a) :
@[protected, instance]
def padic.complete_space {p : } [hp : fact (nat.prime p)] :

### Valuation on ℚ_[p]#

noncomputable def padic.valuation {p : } [hp : fact (nat.prime p)] :

padic.valuation lifts the p-adic valuation on rationals to ℚ_[p].

Equations
@[simp]
theorem padic.valuation_zero {p : } [hp : fact (nat.prime p)] :
@[simp]
theorem padic.valuation_one {p : } [hp : fact (nat.prime p)] :
theorem padic.norm_eq_pow_val {p : } [hp : fact (nat.prime p)] {x : ℚ_[p]} :
@[simp]
theorem padic.valuation_p {p : } [hp : fact (nat.prime p)] :
theorem padic.valuation_map_add {p : } [hp : fact (nat.prime p)] {x y : ℚ_[p]} (hxy : x + y 0) :
(x + y).valuation
@[simp]
theorem padic.valuation_map_mul {p : } [hp : fact (nat.prime p)] {x y : ℚ_[p]} (hx : x 0) (hy : y 0) :
(x * y).valuation =
noncomputable def padic.add_valuation_def {p : } [hp : fact (nat.prime p)] :

The additive p-adic valuation on ℚ_[p], with values in with_top ℤ.

Equations
@[simp]
@[simp]
theorem padic.add_valuation.map_mul {p : } [hp : fact (nat.prime p)] (x y : ℚ_[p]) :
noncomputable def padic.add_valuation {p : } [hp : fact (nat.prime p)] :

The additive p-adic valuation on ℚ_[p], as an add_valuation.

Equations
@[simp]
theorem padic.add_valuation.apply {p : } [hp : fact (nat.prime p)] {x : ℚ_[p]} (hx : x 0) :

### Various characterizations of open unit balls #

theorem padic.norm_le_pow_iff_norm_lt_pow_add_one {p : } [hp : fact (nat.prime p)] (x : ℚ_[p]) (n : ) :
x p ^ n x < p ^ (n + 1)
theorem padic.norm_lt_pow_iff_norm_le_pow_sub_one {p : } [hp : fact (nat.prime p)] (x : ℚ_[p]) (n : ) :
x < p ^ n x p ^ (n - 1)