p-adic numbers

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
• padicNormE : the rational-valued p-adic norm on ℚ_[p]
• Padic.addValuation : the additive p-adic valuation on ℚ_[p], with values in WithTop ℤ

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.

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

simp prefers padicNorm to padicNormE when possible. Since padicNormE 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

• [F. Q. Gouvêa, 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, norm, valuation, cauchy, completion, p-adic completion

def Rat.padicValuation (p : ℕ) [Fact (Nat.Prime p)] : Valuation ℚ (WithZero (Multiplicative ℤ))

The p-adic valuation on rationals, sending p to (exp (-1) : ℤᵐ⁰)

def Int.padicValuation (p : ℕ) [Fact (Nat.Prime p)] : Valuation ℤ (WithZero (Multiplicative ℤ))

The p-adic valuation on integers, sending p to (exp (-1) : ℤᵐ⁰)

theorem Rat.padicValuation_cast (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ) : (padicValuation p) ↑x = (Int.padicValuation p) x

theorem Rat.padicValuation_eq_zero_iff {p : ℕ} [Fact (Nat.Prime p)] {x : ℚ} : (padicValuation p) x = 0 ↔ x = 0

@[simp]

theorem Int.padicValuation_eq_zero_iff {p : ℕ} [Fact (Nat.Prime p)] {x : ℤ} : (padicValuation p) x = 0 ↔ x = 0

@[simp]

theorem Rat.padicValuation_self (p : ℕ) [Fact (Nat.Prime p)] : (padicValuation p) ↑p = WithZero.exp (-1)

@[simp]

theorem Int.padicValuation_self (p : ℕ) [Fact (Nat.Prime p)] : (padicValuation p) ↑p = WithZero.exp (-1)

theorem Int.padicValuation_le_one (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ) : (padicValuation p) x ≤ 1

theorem Int.padicValuation_eq_one_iff {p : ℕ} [Fact (Nat.Prime p)] {x : ℤ} : (padicValuation p) x = 1 ↔ ¬↑p ∣ x

theorem Int.padicValuation_lt_one_iff {p : ℕ} [Fact (Nat.Prime p)] {x : ℤ} : (padicValuation p) x < 1 ↔ ↑p ∣ x

theorem Rat.padicValuation_le_one_iff {p : ℕ} [Fact (Nat.Prime p)] {x : ℚ} : (padicValuation p) x ≤ 1 ↔ ¬p ∣ x.den

theorem Rat.surjective_padicValuation (p : ℕ) [hp : Fact (Nat.Prime p)] : Function.Surjective ⇑(padicValuation p)

@[reducible, inline]

abbrev PadicSeq (p : ℕ) : Type

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

theorem PadicSeq.stationary {p : ℕ} [Fact (Nat.Prime p)] {f : CauSeq ℚ (padicNorm p)} (hf : ¬f ≈ 0) : ∃ (N : ℕ), ∀ (m n : ℕ), N ≤ m → N ≤ n → padicNorm p (↑f n) = padicNorm p (↑f m)

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

noncomputable def PadicSeq.stationaryPoint {p : ℕ} [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) : ℕ

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

theorem PadicSeq.stationaryPoint_spec {p : ℕ} [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) {m n : ℕ} : stationaryPoint hf ≤ m → stationaryPoint hf ≤ n → padicNorm p (↑f n) = padicNorm p (↑f m)

noncomputable def PadicSeq.norm {p : ℕ} [Fact (Nat.Prime p)] (f : PadicSeq p) : ℚ

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

theorem PadicSeq.norm_zero_iff {p : ℕ} [Fact (Nat.Prime p)] (f : PadicSeq p) : f.norm = 0 ↔ f ≈ 0

theorem PadicSeq.equiv_zero_of_val_eq_of_equiv_zero {p : ℕ} [Fact (Nat.Prime p)] {f g : PadicSeq p} (h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)) (hf : f ≈ 0) : g ≈ 0

theorem PadicSeq.norm_nonzero_of_not_equiv_zero {p : ℕ} [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) : f.norm ≠ 0

theorem PadicSeq.norm_eq_norm_app_of_nonzero {p : ℕ} [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) : ∃ (k : ℚ), f.norm = padicNorm p k ∧ k ≠ 0

theorem PadicSeq.not_limZero_const_of_nonzero {p : ℕ} [Fact (Nat.Prime p)] {q : ℚ} (hq : q ≠ 0) : ¬(CauSeq.const (padicNorm p) q).LimZero

theorem PadicSeq.not_equiv_zero_const_of_nonzero {p : ℕ} [Fact (Nat.Prime p)] {q : ℚ} (hq : q ≠ 0) : ¬CauSeq.const (padicNorm p) q ≈ 0

theorem PadicSeq.norm_nonneg {p : ℕ} [Fact (Nat.Prime p)] (f : PadicSeq p) : 0 ≤ f.norm

theorem PadicSeq.lift_index_left_left {p : ℕ} [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) (v2 v3 : ℕ) : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max (stationaryPoint hf) (max v2 v3)))

An auxiliary lemma for manipulating sequence indices.

theorem PadicSeq.lift_index_left {p : ℕ} [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) (v1 v3 : ℕ) : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max v1 (max (stationaryPoint hf) v3)))

An auxiliary lemma for manipulating sequence indices.

theorem PadicSeq.lift_index_right {p : ℕ} [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) (v1 v2 : ℕ) : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max v1 (max v2 (stationaryPoint hf))))

An auxiliary lemma for manipulating sequence indices.

Valuation on PadicSeq

noncomputable def PadicSeq.valuation {p : ℕ} [Fact (Nat.Prime p)] (f : PadicSeq p) : ℤ

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

theorem PadicSeq.norm_eq_zpow_neg_valuation {p : ℕ} [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) : f.norm = ↑p ^ (-f.valuation)

theorem PadicSeq.val_eq_iff_norm_eq {p : ℕ} [Fact (Nat.Prime p)] {f g : PadicSeq p} (hf : ¬f ≈ 0) (hg : ¬g ≈ 0) : f.valuation = g.valuation ↔ f.norm = g.norm

theorem PadicSeq.norm_mul {p : ℕ} [hp : Fact (Nat.Prime p)] (f g : PadicSeq p) : (f * g).norm = f.norm * g.norm

theorem PadicSeq.eq_zero_iff_equiv_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (f : PadicSeq p) : CauSeq.Completion.mk f = 0 ↔ f ≈ 0

theorem PadicSeq.ne_zero_iff_nequiv_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (f : PadicSeq p) : CauSeq.Completion.mk f ≠ 0 ↔ ¬f ≈ 0

theorem PadicSeq.norm_const {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ) : norm (CauSeq.const (padicNorm p) q) = padicNorm p q

theorem PadicSeq.norm_values_discrete {p : ℕ} [hp : Fact (Nat.Prime p)] (a : PadicSeq p) (ha : ¬a ≈ 0) : ∃ (z : ℤ), a.norm = ↑p ^ (-z)

theorem PadicSeq.norm_one {p : ℕ} [hp : Fact (Nat.Prime p)] : norm 1 = 1

theorem PadicSeq.norm_equiv {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p} (hfg : f ≈ g) : f.norm = g.norm

theorem PadicSeq.norm_nonarchimedean {p : ℕ} [hp : Fact (Nat.Prime p)] (f g : PadicSeq p) : (f + g).norm ≤ max f.norm g.norm

theorem PadicSeq.norm_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p} (h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)) : f.norm = g.norm

theorem PadicSeq.norm_neg {p : ℕ} [hp : Fact (Nat.Prime p)] (a : PadicSeq p) : (-a).norm = a.norm

theorem PadicSeq.norm_eq_of_add_equiv_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p} (h : f + g ≈ 0) : f.norm = g.norm

theorem PadicSeq.add_eq_max_of_ne {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p} (hfgne : f.norm ≠ g.norm) : (f + g).norm = max f.norm g.norm

def Padic (p : ℕ) [Fact (Nat.Prime p)] : Type

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

@[implicit_reducible]

noncomputable instance instZeroPadic (p : ℕ) [Fact (Nat.Prime p)] : Zero ℚ_[p]

@[implicit_reducible]

noncomputable instance instOnePadic (p : ℕ) [Fact (Nat.Prime p)] : One ℚ_[p]

@[implicit_reducible]

noncomputable instance instAddPadic (p : ℕ) [Fact (Nat.Prime p)] : Add ℚ_[p]

@[implicit_reducible]

noncomputable instance instNegPadic (p : ℕ) [Fact (Nat.Prime p)] : Neg ℚ_[p]

@[implicit_reducible]

noncomputable instance instSubPadic (p : ℕ) [Fact (Nat.Prime p)] : Sub ℚ_[p]

@[implicit_reducible]

noncomputable instance instMulPadic (p : ℕ) [Fact (Nat.Prime p)] : Mul ℚ_[p]

@[implicit_reducible]

noncomputable instance instDivPadic (p : ℕ) [Fact (Nat.Prime p)] : Div ℚ_[p]

@[implicit_reducible]

noncomputable instance instAddCommGroupPadic (p : ℕ) [Fact (Nat.Prime p)] : AddCommGroup ℚ_[p]

@[implicit_reducible]

noncomputable instance instRingPadic (p : ℕ) [Fact (Nat.Prime p)] : Ring ℚ_[p]

@[implicit_reducible]

noncomputable instance instCommRingPadic (p : ℕ) [Fact (Nat.Prime p)] : CommRing ℚ_[p]

@[implicit_reducible]

noncomputable instance instFieldPadic (p : ℕ) [Fact (Nat.Prime p)] : Field ℚ_[p]

@[implicit_reducible]

noncomputable instance instInhabitedPadic (p : ℕ) [Fact (Nat.Prime p)] : Inhabited ℚ_[p]

def «termℚ_[_]» : Lean.ParserDescr

notation for p-padic rationals

def Padic.mk {p : ℕ} [Fact (Nat.Prime p)] : PadicSeq p → ℚ_[p]

Builds the equivalence class of a Cauchy sequence of rationals.

theorem Padic.zero_def (p : ℕ) [Fact (Nat.Prime p)] : 0 = ⟦0⟧

theorem Padic.mk_eq (p : ℕ) [Fact (Nat.Prime p)] {f g : PadicSeq p} : mk f = mk g ↔ f ≈ g

theorem Padic.const_equiv (p : ℕ) [Fact (Nat.Prime p)] {q r : ℚ} : CauSeq.const (padicNorm p) q ≈ CauSeq.const (padicNorm p) r ↔ q = r

theorem Padic.coe_inj (p : ℕ) [Fact (Nat.Prime p)] {q r : ℚ} : ↑q = ↑r ↔ q = r

instance Padic.instCharZero (p : ℕ) [Fact (Nat.Prime p)] : CharZero ℚ_[p]

theorem Padic.coe_add (p : ℕ) [Fact (Nat.Prime p)] {x y : ℚ} : ↑(x + y) = ↑x + ↑y

theorem Padic.coe_neg (p : ℕ) [Fact (Nat.Prime p)] {x : ℚ} : ↑(-x) = -↑x

theorem Padic.coe_mul (p : ℕ) [Fact (Nat.Prime p)] {x y : ℚ} : ↑(x * y) = ↑x * ↑y

theorem Padic.coe_sub (p : ℕ) [Fact (Nat.Prime p)] {x y : ℚ} : ↑(x - y) = ↑x - ↑y

theorem Padic.coe_div (p : ℕ) [Fact (Nat.Prime p)] {x y : ℚ} : ↑(x / y) = ↑x / ↑y

theorem Padic.coe_one (p : ℕ) [Fact (Nat.Prime p)] : ↑1 = 1

theorem Padic.coe_zero (p : ℕ) [Fact (Nat.Prime p)] : ↑0 = 0

noncomputable def padicNormE {p : ℕ} [hp : Fact (Nat.Prime p)] : AbsoluteValue ℚ_[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 ‖ ‖.

theorem padicNormE.defn {p : ℕ} [Fact (Nat.Prime p)] (f : PadicSeq p) {ε : ℚ} (hε : 0 < ε) : ∃ (N : ℕ), ∀ i ≥ N, padicNormE (Padic.mk f - ↑(↑f i)) < ε

theorem padicNormE.nonarchimedean' {p : ℕ} [Fact (Nat.Prime p)] (q r : ℚ_[p]) : padicNormE (q + r) ≤ max (padicNormE q) (padicNormE r)

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

theorem padicNormE.add_eq_max_of_ne' {p : ℕ} [Fact (Nat.Prime p)] {q r : ℚ_[p]} : padicNormE q ≠ padicNormE r → padicNormE (q + r) = max (padicNormE q) (padicNormE r)

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

@[simp]

theorem padicNormE.eq_padic_norm' {p : ℕ} [Fact (Nat.Prime p)] (q : ℚ) : padicNormE ↑q = padicNorm p q

theorem padicNormE.image' {p : ℕ} [Fact (Nat.Prime p)] {q : ℚ_[p]} : q ≠ 0 → ∃ (n : ℤ), padicNormE q = ↑p ^ (-n)

theorem Padic.rat_dense' {p : ℕ} [Fact (Nat.Prime p)] (q : ℚ_[p]) {ε : ℚ} (hε : 0 < ε) : ∃ (r : ℚ), padicNormE (q - ↑r) < ε

noncomputable def Padic.limSeq {p : ℕ} [Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] ⇑padicNormE) : ℕ → ℚ

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

theorem Padic.exi_rat_seq_conv {p : ℕ} [Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] ⇑padicNormE) {ε : ℚ} (hε : 0 < ε) : ∃ (N : ℕ), ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε

theorem Padic.exi_rat_seq_conv_cauchy {p : ℕ} [Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] ⇑padicNormE) : IsCauSeq (padicNorm p) (limSeq f)

theorem Padic.complete' {p : ℕ} [Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] ⇑padicNormE) : ∃ (q : ℚ_[p]), ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, padicNormE (q - ↑f i) < ε

theorem Padic.complete'' {p : ℕ} [Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] ⇑padicNormE) : ∃ (q : ℚ_[p]), ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, padicNormE (↑f i - q) < ε

@[implicit_reducible]

noncomputable instance Padic.instDist (p : ℕ) [Fact (Nat.Prime p)] : Dist ℚ_[p]

instance Padic.instIsUltrametricDist (p : ℕ) [Fact (Nat.Prime p)] : IsUltrametricDist ℚ_[p]

@[implicit_reducible]

noncomputable instance Padic.metricSpace (p : ℕ) [Fact (Nat.Prime p)] : MetricSpace ℚ_[p]

@[implicit_reducible]

noncomputable instance Padic.instNorm (p : ℕ) [Fact (Nat.Prime p)] : Norm ℚ_[p]

@[implicit_reducible]

noncomputable instance Padic.normedField (p : ℕ) [Fact (Nat.Prime p)] : NormedField ℚ_[p]

instance Padic.isAbsoluteValue (p : ℕ) [Fact (Nat.Prime p)] : IsAbsoluteValue fun (a : ℚ_[p]) => ‖a‖

theorem Padic.rat_dense (p : ℕ) [Fact (Nat.Prime p)] (q : ℚ_[p]) {ε : ℝ} (hε : 0 < ε) : ∃ (r : ℚ), ‖q - ↑r‖ < ε

theorem Padic.denseRange_ratCast (p : ℕ) [Fact (Nat.Prime p)] : DenseRange Rat.cast

theorem Padic.padicNormE.mul {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℚ_[p]) : ‖q * r‖ = ‖q‖ * ‖r‖

theorem Padic.padicNormE.is_norm {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ_[p]) : ↑(padicNormE q) = ‖q‖

theorem Padic.nonarchimedean {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℚ_[p]) : ‖q + r‖ ≤ max ‖q‖ ‖r‖

theorem Padic.add_eq_max_of_ne {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ_[p]} (h : ‖q‖ ≠ ‖r‖) : ‖q + r‖ = max ‖q‖ ‖r‖

@[simp]

theorem Padic.eq_padicNorm {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ) : ‖↑q‖ = ↑(padicNorm p q)

@[simp]

theorem Padic.norm_p {p : ℕ} [hp : Fact (Nat.Prime p)] : ‖↑p‖ = (↑p)⁻¹

theorem Padic.norm_p_lt_one {p : ℕ} [hp : Fact (Nat.Prime p)] : ‖↑p‖ < 1

@[simp]

theorem Padic.norm_p_zpow {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℤ) : ‖↑p ^ n‖ = ↑p ^ (-n)

@[simp]

theorem Padic.norm_p_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : ‖↑p ^ n‖ = ↑p ^ (-↑n)

@[implicit_reducible]

noncomputable instance Padic.instNontriviallyNormedField {p : ℕ} [hp : Fact (Nat.Prime p)] : NontriviallyNormedField ℚ_[p]

theorem Padic.padicNormE.image {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ_[p]} : q ≠ 0 → ∃ (n : ℤ), ‖q‖ = ↑(↑p ^ (-n))

theorem Padic.padicNormE.is_rat {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ_[p]) : ∃ (q' : ℚ), ‖q‖ = ↑q'

noncomputable def Padic.ratNorm {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ_[p]) : ℚ

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

The lemma padicNormE.eq_ratNorm asserts ‖q‖ = ratNorm q.

theorem Padic.eq_ratNorm {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ_[p]) : ‖q‖ = ↑q.ratNorm

theorem Padic.norm_rat_le_one {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} : ¬p ∣ q.den → ‖↑q‖ ≤ 1

theorem Padic.norm_int_le_one {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ) : ‖↑z‖ ≤ 1

@[simp]

theorem Padic.norm_intCast_lt_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℤ} : ‖↑k‖ < 1 ↔ ↑p ∣ k

@[simp]

theorem Padic.norm_natCast_lt_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} : ‖↑n‖ < 1 ↔ p ∣ n

@[simp]

theorem Padic.norm_intCast_eq_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ} : ‖↑z‖ = 1 ↔ IsCoprime z ↑p

@[simp]

theorem Padic.norm_natCast_eq_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} : ‖↑n‖ = 1 ↔ p.Coprime n

theorem Padic.norm_int_le_pow_iff_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ) (n : ℕ) : ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

theorem Padic.norm_eq_of_norm_add_lt_right {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℚ_[p]} (h : ‖z1 + z2‖ < ‖z2‖) : ‖z1‖ = ‖z2‖

theorem Padic.norm_eq_of_norm_add_lt_left {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℚ_[p]} (h : ‖z1 + z2‖ < ‖z1‖) : ‖z1‖ = ‖z2‖

theorem Padic.norm_eq_of_norm_sub_lt_right {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℚ_[p]} (h : ‖z1 - z2‖ < ‖z2‖) : ‖z1‖ = ‖z2‖

theorem Padic.norm_eq_of_norm_sub_lt_left {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℚ_[p]} (h : ‖z1 - z2‖ < ‖z1‖) : ‖z1‖ = ‖z2‖

@[simp]

theorem Padic.norm_natCast_p_sub_one {p : ℕ} [hp : Fact (Nat.Prime p)] : ‖↑(p - 1)‖ = 1

instance Padic.complete {p : ℕ} [hp : Fact (Nat.Prime p)] : CauSeq.IsComplete ℚ_[p] norm

theorem Padic.padicNormE_lim_le {p : ℕ} [hp : Fact (Nat.Prime p)] {f : CauSeq ℚ_[p] norm} {a : ℝ} (ha : 0 < a) (hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a) : ‖f.lim‖ ≤ a

instance Padic.instCompleteSpace {p : ℕ} [hp : Fact (Nat.Prime p)] : CompleteSpace ℚ_[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].

@[simp]

theorem Padic.valuation_zero {p : ℕ} [hp : Fact (Nat.Prime p)] : valuation 0 = 0

theorem Padic.norm_eq_zpow_neg_valuation {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℚ_[p]} : x ≠ 0 → ‖x‖ = ↑p ^ (-x.valuation)

@[simp]

theorem Padic.valuation_ratCast {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ) : (↑q).valuation = padicValRat p q

@[simp]

theorem Padic.valuation_intCast {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℤ) : (↑n).valuation = ↑(padicValInt p n)

@[simp]

theorem Padic.valuation_natCast {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : (↑n).valuation = ↑(padicValNat p n)

@[simp]

theorem Padic.valuation_ofNat {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).valuation = ↑(padicValNat p n)

@[simp]

theorem Padic.valuation_one {p : ℕ} [hp : Fact (Nat.Prime p)] : valuation 1 = 0

theorem Padic.valuation_p {p : ℕ} [hp : Fact (Nat.Prime p)] : (↑p).valuation = 1

theorem Padic.le_valuation_add {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℚ_[p]} (hxy : x + y ≠ 0) : min x.valuation y.valuation ≤ (x + y).valuation

@[simp]

theorem Padic.valuation_mul {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℚ_[p]} (hx : x ≠ 0) (hy : y ≠ 0) : (x * y).valuation = x.valuation + y.valuation

@[simp]

theorem Padic.valuation_inv {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) : x⁻¹.valuation = -x.valuation

@[simp]

theorem Padic.valuation_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (n : ℕ) : (x ^ n).valuation = ↑n * x.valuation

@[simp]

theorem Padic.valuation_zpow {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (n : ℤ) : (x ^ n).valuation = n * x.valuation

noncomputable def Padic.addValuationDef {p : ℕ} [hp : Fact (Nat.Prime p)] : ℚ_[p] → WithTop ℤ

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

@[simp]

theorem Padic.AddValuation.map_zero {p : ℕ} [hp : Fact (Nat.Prime p)] : addValuationDef 0 = ⊤

@[simp]

theorem Padic.AddValuation.map_one {p : ℕ} [hp : Fact (Nat.Prime p)] : addValuationDef 1 = 0

theorem Padic.AddValuation.map_mul {p : ℕ} [hp : Fact (Nat.Prime p)] (x y : ℚ_[p]) : (x * y).addValuationDef = x.addValuationDef + y.addValuationDef

theorem Padic.AddValuation.map_add {p : ℕ} [hp : Fact (Nat.Prime p)] (x y : ℚ_[p]) : min x.addValuationDef y.addValuationDef ≤ (x + y).addValuationDef

noncomputable def Padic.mulValuation {p : ℕ} [hp : Fact (Nat.Prime p)] : Valuation ℚ_[p] (WithZero (Multiplicative ℤ))

The p-adic valuation on ℚ_[p], as a Valuation, bundled Padic.valuation.

@[simp]

theorem Padic.mulValuation_toFun {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) : mulValuation x = if x = 0 then 0 else WithZero.exp (-x.valuation)

theorem Padic.comap_mulValuation_eq_padicValuation {p : ℕ} [hp : Fact (Nat.Prime p)] : Valuation.comap (Rat.castHom ℚ_[p]) mulValuation = Rat.padicValuation p

theorem Padic.comap_mulValuation_eq_int_padicValuation {p : ℕ} [hp : Fact (Nat.Prime p)] : Valuation.comap (Int.castRingHom ℚ_[p]) mulValuation = Int.padicValuation p

theorem Padic.norm_eq_zpow_log_mulValuation {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℚ_[p]} (hx : x ≠ 0) : ‖x‖ = ↑p ^ (mulValuation x).log

noncomputable def Padic.addValuation {p : ℕ} [hp : Fact (Nat.Prime p)] : AddValuation ℚ_[p] (WithTop ℤ)

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

@[simp]

theorem Padic.addValuation.apply {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℚ_[p]} (hx : x ≠ 0) : addValuation 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