mathlib3 documentation

number_theory.padics.padic_numbers

p-adic numbers #

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.

References #

Tags #

p-adic, p adic, padic, norm, valuation, cauchy, completion, p-adic completion

@[reducible]

def padic_seq (p : ℕ) :

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

Equations

padic_seq p = cau_seq ℚ (padic_norm p)

theorem padic_seq.stationary {p : ℕ} [fact (nat.prime p)] {f : cau_seq ℚ (padic_norm p)} (hf : ¬f ≈ 0) :

∃ (N : ℕ), ∀ (m n : ℕ), N ≤ m → N ≤ n → padic_norm p (⇑f n) = padic_norm p (⇑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

padic_seq.stationary_point hf = classical.some _

theorem padic_seq.stationary_point_spec {p : ℕ} [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f ≈ 0) {m n : ℕ} :

padic_seq.stationary_point hf ≤ m → padic_seq.stationary_point hf ≤ n → padic_norm p (⇑f n) = padic_norm p (⇑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

f.norm = dite (f ≈ 0) (λ (hf : f ≈ 0), 0) (λ (hf : ¬f ≈ 0), padic_norm p (⇑f (padic_seq.stationary_point hf)))

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 : ℕ), padic_norm p (⇑f k) = padic_norm p (⇑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) :

theorem padic_seq.norm_eq_norm_app_of_nonzero {p : ℕ} [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f ≈ 0) :

∃ (k : ℚ), f.norm = padic_norm p k ∧ k ≠ 0

theorem padic_seq.not_lim_zero_const_of_nonzero {p : ℕ} [fact (nat.prime p)] {q : ℚ} (hq : q ≠ 0) :

¬(cau_seq.const (padic_norm p) q).lim_zero

theorem padic_seq.not_equiv_zero_const_of_nonzero {p : ℕ} [fact (nat.prime p)] {q : ℚ} (hq : q ≠ 0) :

¬cau_seq.const (padic_norm p) q ≈ 0

theorem padic_seq.norm_nonneg {p : ℕ} [fact (nat.prime p)] (f : padic_seq p) :

theorem padic_seq.lift_index_left_left {p : ℕ} [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f ≈ 0) (v2 v3 : ℕ) :

padic_norm p (⇑f (padic_seq.stationary_point hf)) = padic_norm p (⇑f (linear_order.max (padic_seq.stationary_point hf) (linear_order.max v2 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 : ℕ) :

padic_norm p (⇑f (padic_seq.stationary_point hf)) = padic_norm p (⇑f (linear_order.max v1 (linear_order.max (padic_seq.stationary_point hf) 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 : ℕ) :

padic_norm p (⇑f (padic_seq.stationary_point hf)) = padic_norm p (⇑f (linear_order.max v1 (linear_order.max v2 (padic_seq.stationary_point hf))))

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

f.valuation = dite (f ≈ 0) (λ (hf : f ≈ 0), 0) (λ (hf : ¬f ≈ 0), padic_val_rat p (⇑f (padic_seq.stationary_point hf)))

theorem padic_seq.norm_eq_pow_val {p : ℕ} [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f ≈ 0) :

f.norm = ↑p ^ -f.valuation

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.valuation = g.valuation ↔ f.norm = g.norm

meta def tactic.interactive.padic_index_simp (l : interactive.parse interactive.types.pexpr_list) (at_ : interactive.parse interactive.types.location) :

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) :

cau_seq.completion.mk f = 0 ↔ f ≈ 0

theorem padic_seq.ne_zero_iff_nequiv_zero {p : ℕ} [hp : fact (nat.prime p)] (f : padic_seq p) :

cau_seq.completion.mk f ≠ 0 ↔ ¬f ≈ 0

theorem padic_seq.norm_const {p : ℕ} [hp : fact (nat.prime p)] (q : ℚ) :

padic_seq.norm (cau_seq.const (padic_norm p) q) = padic_norm p 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 ≤ linear_order.max f.norm g.norm

theorem padic_seq.norm_eq {p : ℕ} [hp : fact (nat.prime p)] {f g : padic_seq p} (h : ∀ (k : ℕ), padic_norm p (⇑f k) = padic_norm p (⇑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 = linear_order.max f.norm 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

ℚ_[p] = cau_seq.completion.Cauchy (padic_norm p)

Instances for padic

@[protected, instance]

noncomputable def padic.field {p : ℕ} [fact (nat.prime p)] :

Equations

padic.field = cau_seq.completion.Cauchy.field

@[protected, instance]

noncomputable def padic.inhabited {p : ℕ} [fact (nat.prime p)] :

inhabited ℚ_[p]

Equations

padic.inhabited = {default := 0}

@[protected, instance]

def padic.comm_ring {p : ℕ} [fact (nat.prime p)] :

comm_ring ℚ_[p]

Equations

padic.comm_ring = cau_seq.completion.Cauchy.comm_ring

@[protected, instance]

def padic.ring {p : ℕ} [fact (nat.prime p)] :

Equations

padic.ring = cau_seq.completion.Cauchy.ring

@[protected, instance]

def padic.has_zero {p : ℕ} [fact (nat.prime p)] :

has_zero ℚ_[p]

Equations

padic.has_zero = mul_zero_class.to_has_zero ℚ_[p]

@[protected, instance]

def padic.has_one {p : ℕ} [fact (nat.prime p)] :

has_one ℚ_[p]

Equations

padic.has_one = add_monoid_with_one.to_has_one ℚ_[p]

@[protected, instance]

def padic.has_add {p : ℕ} [fact (nat.prime p)] :

has_add ℚ_[p]

Equations

padic.has_add = distrib.to_has_add ℚ_[p]

@[protected, instance]

def padic.has_mul {p : ℕ} [fact (nat.prime p)] :

has_mul ℚ_[p]

Equations

padic.has_mul = distrib.to_has_mul ℚ_[p]

@[protected, instance]

def padic.has_sub {p : ℕ} [fact (nat.prime p)] :

has_sub ℚ_[p]

Equations

padic.has_sub = sub_neg_monoid.to_has_sub ℚ_[p]

@[protected, instance]

def padic.has_neg {p : ℕ} [fact (nat.prime p)] :

has_neg ℚ_[p]

Equations

padic.has_neg = sub_neg_monoid.to_has_neg ℚ_[p]

@[protected, instance]

noncomputable def padic.has_div {p : ℕ} [fact (nat.prime p)] :

has_div ℚ_[p]

Equations

padic.has_div = div_inv_monoid.to_has_div ℚ_[p]

@[protected, instance]

def padic.add_comm_group {p : ℕ} [fact (nat.prime p)] :

add_comm_group ℚ_[p]

Equations

padic.add_comm_group = non_unital_non_assoc_ring.to_add_comm_group ℚ_[p]

def padic.mk {p : ℕ} [fact (nat.prime p)] :

padic_seq p → ℚ_[p]

Builds the equivalence class of a Cauchy sequence of rationals.

Equations

padic.mk = quotient.mk

theorem padic.zero_def (p : ℕ) [fact (nat.prime p)] :

theorem padic.mk_eq (p : ℕ) [fact (nat.prime p)] {f g : padic_seq p} :

padic.mk f = padic.mk g ↔ f ≈ g

theorem padic.const_equiv (p : ℕ) [fact (nat.prime p)] {q r : ℚ} :

cau_seq.const (padic_norm p) q ≈ cau_seq.const (padic_norm p) 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)] :

char_zero ℚ_[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)] :

absolute_value ℚ_[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

padic_norm_e = {to_mul_hom := {to_fun := quotient.lift padic_seq.norm padic_seq.norm_equiv, map_mul' := _}, nonneg' := _, eq_zero' := _, add_le' := _}

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]) :

⇑padic_norm_e (q + r) ≤ linear_order.max (⇑padic_norm_e q) (⇑padic_norm_e r)

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]} :

⇑padic_norm_e q ≠ ⇑padic_norm_e r → ⇑padic_norm_e (q + r) = linear_order.max (⇑padic_norm_e q) (⇑padic_norm_e r)

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 : ℚ) :

⇑padic_norm_e ↑q = padic_norm p q

@[protected]

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

q ≠ 0 → (∃ (n : ℤ), ⇑padic_norm_e q = ↑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 : cau_seq ℚ_[p] ⇑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

padic.lim_seq f = λ (n : ℕ), classical.some _

theorem padic.exi_rat_seq_conv {p : ℕ} [fact (nat.prime p)] (f : cau_seq ℚ_[p] ⇑padic_norm_e) {ε : ℚ} (hε : 0 < ε) :

∃ (N : ℕ), ∀ (i : ℕ), i ≥ N → ⇑padic_norm_e (⇑f i - ↑(padic.lim_seq f i)) < ε

theorem padic.exi_rat_seq_conv_cauchy {p : ℕ} [fact (nat.prime p)] (f : cau_seq ℚ_[p] ⇑padic_norm_e) :

is_cau_seq (padic_norm p) (padic.lim_seq f)

theorem padic.complete' {p : ℕ} [fact (nat.prime p)] (f : cau_seq ℚ_[p] ⇑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)] :

has_dist ℚ_[p]

Equations

padic.has_dist p = {dist := λ (x y : ℚ_[p]), ↑(⇑padic_norm_e (x - y))}

@[protected, instance]

noncomputable def padic.metric_space (p : ℕ) [fact (nat.prime p)] :

metric_space ℚ_[p]

Equations

padic.metric_space p = {to_pseudo_metric_space := {to_has_dist := {dist := has_dist.dist (padic.has_dist p)}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : ℚ_[p]), ↑⟨has_dist.dist x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist has_dist.dist _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist has_dist.dist _ _ _, cobounded_sets := _}, eq_of_dist_eq_zero := _}

@[protected, instance]

noncomputable def padic.has_norm (p : ℕ) [fact (nat.prime p)] :

has_norm ℚ_[p]

Equations

padic.has_norm p = {norm := λ (x : ℚ_[p]), ↑(⇑padic_norm_e x)}

@[protected, instance]

noncomputable def padic.normed_field (p : ℕ) [fact (nat.prime p)] :

normed_field ℚ_[p]

Equations

padic.normed_field p = {to_has_norm := {norm := has_norm.norm (padic.has_norm p)}, to_field := {add := field.add padic.field, add_assoc := _, zero := field.zero padic.field, zero_add := _, add_zero := _, nsmul := field.nsmul padic.field, nsmul_zero' := _, nsmul_succ' := _, neg := field.neg padic.field, sub := field.sub padic.field, sub_eq_add_neg := _, zsmul := field.zsmul padic.field, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := field.int_cast padic.field, nat_cast := field.nat_cast padic.field, one := field.one padic.field, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := field.mul padic.field, mul_assoc := _, one_mul := _, mul_one := _, npow := field.npow padic.field, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := field.inv padic.field, div := field.div padic.field, div_eq_mul_inv := _, zpow := field.zpow padic.field, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := field.rat_cast padic.field, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := field.qsmul padic.field, qsmul_eq_mul' := _}, to_metric_space := {to_pseudo_metric_space := metric_space.to_pseudo_metric_space (padic.metric_space p), eq_of_dist_eq_zero := _}, dist_eq := _, norm_mul' := _}

@[protected, instance]

def padic.is_absolute_value (p : ℕ) [fact (nat.prime p)] :

is_absolute_value (λ (a : ℚ_[p]), ‖a‖)

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]) :

‖q * r‖ = ‖q‖ * ‖r‖

@[protected]

theorem padic_norm_e.is_norm {p : ℕ} [hp : fact (nat.prime p)] (q : ℚ_[p]) :

↑(⇑padic_norm_e q) = ‖q‖

theorem padic_norm_e.nonarchimedean {p : ℕ} [hp : fact (nat.prime p)] (q r : ℚ_[p]) :

‖q + r‖ ≤ linear_order.max ‖q‖ ‖r‖

theorem padic_norm_e.add_eq_max_of_ne {p : ℕ} [hp : fact (nat.prime p)] {q r : ℚ_[p]} (h : ‖q‖ ≠ ‖r‖) :

‖q + r‖ = linear_order.max ‖q‖ ‖r‖

@[simp]

theorem padic_norm_e.eq_padic_norm {p : ℕ} [hp : fact (nat.prime p)] (q : ℚ) :

‖↑q‖ = ↑(padic_norm p q)

@[simp]

theorem padic_norm_e.norm_p {p : ℕ} [hp : fact (nat.prime p)] :

‖↑p‖ = (↑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 : ℤ) :

‖↑p ^ n‖ = ↑p ^ -n

@[simp]

theorem padic_norm_e.norm_p_pow {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) :

‖↑p ^ n‖ = ↑p ^ -↑n

@[protected, instance]

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

nontrivially_normed_field ℚ_[p]

Equations

padic_norm_e.padic.nontrivially_normed_field = {to_normed_field := {to_has_norm := normed_field.to_has_norm (padic.normed_field p), to_field := normed_field.to_field (padic.normed_field p), to_metric_space := normed_field.to_metric_space (padic.normed_field p), dist_eq := _, norm_mul' := _}, non_trivial := _}

@[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

padic_norm_e.rat_norm q = classical.some _

theorem padic_norm_e.eq_rat_norm {p : ℕ} [hp : fact (nat.prime p)] (q : ℚ_[p]) :

‖q‖ = ↑(padic_norm_e.rat_norm q)

theorem padic_norm_e.norm_rat_le_one {p : ℕ} [hp : fact (nat.prime p)] {q : ℚ} (hq : ¬p ∣ q.denom) :

‖↑q‖ ≤ 1

theorem padic_norm_e.norm_int_le_one {p : ℕ} [hp : fact (nat.prime p)] (z : ℤ) :

‖↑z‖ ≤ 1

theorem padic_norm_e.norm_int_lt_one_iff_dvd {p : ℕ} [hp : fact (nat.prime p)] (k : ℤ) :

‖↑k‖ < 1 ↔ ↑p ∣ k

theorem padic_norm_e.norm_int_le_pow_iff_dvd {p : ℕ} [hp : fact (nat.prime p)] (k : ℤ) (n : ℕ) :

‖↑k‖ ≤ ↑p ^ -↑n ↔ ↑(p ^ n) ∣ k

theorem padic_norm_e.eq_of_norm_add_lt_right {p : ℕ} [hp : fact (nat.prime p)] {z1 z2 : ℚ_[p]} (h : ‖z1 + z2‖ < ‖z2‖) :

‖z1‖ = ‖z2‖

theorem padic_norm_e.eq_of_norm_add_lt_left {p : ℕ} [hp : fact (nat.prime p)] {z1 z2 : ℚ_[p]} (h : ‖z1 + z2‖ < ‖z1‖) :

‖z1‖ = ‖z2‖

@[protected, instance]

def padic.complete {p : ℕ} [hp : fact (nat.prime p)] :

cau_seq.is_complete ℚ_[p] has_norm.norm

theorem padic.padic_norm_e_lim_le {p : ℕ} [hp : fact (nat.prime p)] {f : cau_seq ℚ_[p] has_norm.norm} {a : ℝ} (ha : 0 < a) (hf : ∀ (i : ℕ), ‖⇑f i‖ ≤ a) :

‖f.lim ‖ ≤ a

@[protected, instance]

def padic.complete_space {p : ℕ} [hp : fact (nat.prime p)] :

complete_space ℚ_[p]

Valuation on `ℚ_[p]` #

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

ℚ_[p] → ℤ

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

Equations

padic.valuation = quotient.lift padic_seq.valuation padic.valuation._proof_1

@[simp]

theorem padic.valuation_zero {p : ℕ} [hp : fact (nat.prime p)] :

0.valuation = 0

@[simp]

theorem padic.valuation_one {p : ℕ} [hp : fact (nat.prime p)] :

1.valuation = 0

theorem padic.norm_eq_pow_val {p : ℕ} [hp : fact (nat.prime p)] {x : ℚ_[p]} :

x ≠ 0 → ‖x‖ = ↑p ^ -x.valuation

@[simp]

theorem padic.valuation_p {p : ℕ} [hp : fact (nat.prime p)] :

↑p.valuation = 1

theorem padic.valuation_map_add {p : ℕ} [hp : fact (nat.prime p)] {x y : ℚ_[p]} (hxy : x + y ≠ 0) :

linear_order.min x.valuation y.valuation ≤ (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 = x.valuation + y.valuation

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

ℚ_[p] → with_top ℤ

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

Equations

padic.add_valuation_def = λ (x : ℚ_[p]), ite (x = 0) ⊤ ↑(x.valuation)

@[simp]

theorem padic.add_valuation.map_zero {p : ℕ} [hp : fact (nat.prime p)] :

0.add_valuation_def = ⊤

@[simp]

theorem padic.add_valuation.map_one {p : ℕ} [hp : fact (nat.prime p)] :

1.add_valuation_def = 0

theorem padic.add_valuation.map_mul {p : ℕ} [hp : fact (nat.prime p)] (x y : ℚ_[p]) :

(x * y).add_valuation_def = x.add_valuation_def + y.add_valuation_def

theorem padic.add_valuation.map_add {p : ℕ} [hp : fact (nat.prime p)] (x y : ℚ_[p]) :

linear_order.min x.add_valuation_def y.add_valuation_def ≤ (x + y).add_valuation_def

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

add_valuation ℚ_[p] (with_top ℤ)

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

Equations

padic.add_valuation = add_valuation.of padic.add_valuation_def padic.add_valuation.map_zero padic.add_valuation.map_one padic.add_valuation.map_add padic.add_valuation.map_mul

@[simp]

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

⇑padic.add_valuation x = ↑(x.valuation)

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)

theorem padic.norm_le_one_iff_val_nonneg {p : ℕ} [hp : fact (nat.prime p)] (x : ℚ_[p]) :

‖x‖ ≤ 1 ↔ 0 ≤ x.valuation