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.

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

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]

Tags

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

@[reducible]

def PadicSeq (p : ℕ) : Type

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

Equations

• PadicSeq p = CauSeq ℚ (padicNorm p)

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.

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.

Equations

• PadicSeq.stationaryPoint hf = Classical.choose ⋯

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

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.

Equations

• PadicSeq.norm f = if hf : f ≈ 0 then 0 else padicNorm p (↑f (PadicSeq.stationaryPoint hf))

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

theorem PadicSeq.equiv_zero_of_val_eq_of_equiv_zero {p : ℕ} [Fact (Nat.Prime p)] {f : PadicSeq p} {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) : PadicSeq.norm f ≠ 0

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

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

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 ≤ PadicSeq.norm f

theorem PadicSeq.lift_index_left_left {p : ℕ} [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) (v2 : ℕ) (v3 : ℕ) : padicNorm p (↑f (PadicSeq.stationaryPoint hf)) = padicNorm p (↑f (max (PadicSeq.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 (PadicSeq.stationaryPoint hf)) = padicNorm p (↑f (max v1 (max (PadicSeq.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 (PadicSeq.stationaryPoint hf)) = padicNorm p (↑f (max v1 (max v2 (PadicSeq.stationaryPoint hf))))

An auxiliary lemma for manipulating sequence indices.

Valuation on PadicSeq

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.

Equations

• PadicSeq.valuation f = if hf : f ≈ 0 then 0 else padicValRat p (↑f (PadicSeq.stationaryPoint hf))

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

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

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

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 : ℚ) : PadicSeq.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 : ℤ), PadicSeq.norm a = ↑p ^ (-z)

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

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

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

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

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

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

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

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.

Equations

• ℚ_[p] = CauSeq.Completion.Cauchy (padicNorm p)

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

notation for p-padic rationals

Equations

• One or more equations did not get rendered due to their size.

instance Padic.field {p : ℕ} [Fact (Nat.Prime p)] : Field ℚ_[p]

Equations

• Padic.field = CauSeq.Completion.Cauchy.field

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

Equations

• Padic.instInhabitedPadic = { default := 0 }

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

Equations

• Padic.instCommRingPadic = CauSeq.Completion.Cauchy.commRing

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

Equations

• Padic.instRingPadic = CauSeq.Completion.Cauchy.ring

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

Equations

• Padic.instZeroPadic = inferInstance

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

Equations

• Padic.instOnePadic = inferInstance

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

Equations

• Padic.instAddPadic = inferInstance

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

Equations

• Padic.instMulPadic = inferInstance

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

Equations

• Padic.instSubPadic = inferInstance

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

Equations

• Padic.instNegPadic = inferInstance

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

Equations

• Padic.instDivPadic = inferInstance

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

Equations

• Padic.instAddCommGroupPadic = inferInstance

def Padic.mk {p : ℕ} [Fact (Nat.Prime p)] : PadicSeq 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)] : 0 = ⟦0⟧

theorem Padic.mk_eq (p : ℕ) [Fact (Nat.Prime p)] {f : PadicSeq p} {g : PadicSeq p} : Padic.mk f = Padic.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.instCharZeroPadicToAddMonoidWithOneToAddGroupWithOneInstRingPadic (p : ℕ) [Fact (Nat.Prime p)] : CharZero ℚ_[p]

Equations

• ⋯ = ⋯

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

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

Equations

• padicNormE = { toMulHom := { toFun := Quotient.lift PadicSeq.norm ⋯, map_mul' := ⋯ }, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }

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 : ℚ_[p]) (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 : ℚ_[p]} {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) < ε

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.

Equations

• Padic.limSeq f n = Classical.choose ⋯

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

theorem Padic.exi_rat_seq_conv_cauchy {p : ℕ} [Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] ⇑padicNormE) : IsCauSeq (padicNorm p) (Padic.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) < ε

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

Equations

• Padic.instDistPadic p = { dist := fun (x y : ℚ_[p]) => ↑(padicNormE (x - y)) }

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

Equations

• Padic.metricSpace p = MetricSpace.mk ⋯

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

Equations

• Padic.instNormPadic p = { norm := fun (x : ℚ_[p]) => ↑(padicNormE x) }

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

Equations

• Padic.normedField p = let __src := Padic.field; let __src_1 := Padic.metricSpace p; NormedField.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

instance padicNormE.instNontriviallyNormedFieldPadic {p : ℕ} [hp : Fact (Nat.Prime p)] : NontriviallyNormedField ℚ_[p]

Equations

• padicNormE.instNontriviallyNormedFieldPadic = let __src := Padic.normedField p; NontriviallyNormedField.mk ⋯

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

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

def padicNormE.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.

Equations

• padicNormE.ratNorm q = Classical.choose ⋯

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

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

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

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

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

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

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

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

Equations

• ⋯ = ⋯

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

instance Padic.instCompleteSpacePadicToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingNormedField {p : ℕ} [hp : Fact (Nat.Prime p)] : CompleteSpace ℚ_[p]

Equations

• ⋯ = ⋯

Valuation on ℚ_[p]

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 PadicSeq.valuation ⋯

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

Equations

• Padic.addValuationDef x = if x = 0 then ⊤ else ↑(Padic.valuation x)

@[simp]

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

@[simp]

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

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

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

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

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

Equations

• Padic.addValuation = AddValuation.of Padic.addValuationDef ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Padic.addValuation.apply {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℚ_[p]} (hx : x ≠ 0) : Padic.addValuation x = ↑(Padic.valuation x)

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 ≤ Padic.valuation x