def Converges {X : Type u_1} [PseudoMetricSpace X] (u : ℕ → X) : Prop

@[reducible, inline]

abbrev IsCompleteSpace (X : Type u_1) [UniformSpace X] : Prop

@[reducible, inline]

abbrev IsTopologicalAddGroupDef (G : Type u_1) [AddGroup G] [TopologicalSpace G] : Prop

@[reducible, inline]

abbrev MetricCompletion (X : Type u_1) [UniformSpace X] : Type u_1

theorem completion_universal_property (K : Type u_1) [Field K] (v : AbsoluteValue K ℝ) (L : Type u_2) [Field L] [UniformSpace L] [CompleteSpace L] [T0Space L] [IsTopologicalRing L] [IsUniformAddGroup L] (f : WithAbs v →+* L) (hf : Continuous ⇑f) (hf_inj : Function.Injective ⇑f) : ∃ (g : UniformSpace.Completion (WithAbs v) →+* L), Continuous ⇑g ∧ (∀ (x : WithAbs v), g ↑x = f x) ∧ ∀ (g' : UniformSpace.Completion (WithAbs v) →+* L), Continuous ⇑g' → (∀ (x : WithAbs v), g' ↑x = f x) → ⇑g' = ⇑g

theorem weak_approximation_theorem {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (v : ι → AbsoluteValue K ℝ) (hv_nontrivial : ∀ (i : ι), (v i).IsNontrivial) (hv_ineq : ∀ (i j : ι), i ≠ j → ¬(v i).IsEquiv (v j)) (a : ι → K) (ε : ι → ℝ) (hε : ∀ (i : ι), 0 < ε i) : ∃ (x : K), ∀ (i : ι), (v i) (x - a i) < ε i

@[reducible]

noncomputable def AbsoluteValue.inducedTopology {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : TopologicalSpace K

theorem absoluteValue_same_topology_iff_equiv {K : Type u_1} [Field K] (v w : AbsoluteValue K ℝ) : v.inducedTopology = w.inducedTopology ↔ v.IsEquiv w

def DiscreteValuation.ExtendsWithIndex {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (w : Valuation L (WithZero (Multiplicative ℤ))) (v : Valuation K (WithZero (Multiplicative ℤ))) (e : ℕ) : Prop

theorem intValuation_algebraMap_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Algebra R S] [FaithfulSMul R S] (P : IsDedekindDomain.HeightOneSpectrum R) (Q : IsDedekindDomain.HeightOneSpectrum S) [Q.asIdeal.LiesOver P.asIdeal] (r : R) : Q.intValuation ((algebraMap R S) r) = P.intValuation r ^ P.asIdeal.ramificationIdx Q.asIdeal

theorem valuation_extends_with_ramificationIdx {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Algebra R S] [FaithfulSMul R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u_4) [Field L] [Algebra S L] [IsFractionRing S L] [Algebra R L] [IsScalarTower R S L] [Algebra K L] [IsScalarTower R K L] (P : IsDedekindDomain.HeightOneSpectrum R) (Q : IsDedekindDomain.HeightOneSpectrum S) [Q.asIdeal.LiesOver P.asIdeal] (x : K) : (IsDedekindDomain.HeightOneSpectrum.valuation L Q) ((algebraMap K L) x) = (IsDedekindDomain.HeightOneSpectrum.valuation K P) x ^ P.asIdeal.ramificationIdx Q.asIdeal