p-adic numbers with a valuative relation

Tags

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

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

Equations

• Padic.instValuativeRel = ValuativeRel.ofValuation Padic.mulValuation

instance Padic.instCompatibleWithZeroMultiplicativeIntMulValuation {p : ℕ} [hp : Fact (Nat.Prime p)] : mulValuation.Compatible

theorem Padic.valuation_p_ne_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {Γ₀ : Type u_1} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation ℚ_[p] Γ₀) [v.Compatible] : v ↑p ≠ 0

@[simp]

theorem Padic.valuation_p_lt_one {p : ℕ} [hp : Fact (Nat.Prime p)] {Γ₀ : Type u_1} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation ℚ_[p] Γ₀) [v.Compatible] : v ↑p < 1

instance Padic.instIsNontrivial {p : ℕ} [hp : Fact (Nat.Prime p)] : ValuativeRel.IsNontrivial ℚ_[p]