class IsLocalField (K : Type u_1) extends NontriviallyNormedField K : Type u_1

• norm : K → ℝ
• add : K → K → K
• add_assoc (a b c : K) : a + b + c = a + (b + c)
• zero : K
• zero_add (a : K) : 0 + a = a
• add_zero (a : K) : a + 0 = a
• nsmul : ℕ → K → K
• nsmul_zero (x : K) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : K) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : K) : a + b = b + a
• mul : K → K → K
• left_distrib (a b c : K) : a * (b + c) = a * b + a * c
• right_distrib (a b c : K) : (a + b) * c = a * c + b * c
• zero_mul (a : K) : 0 * a = 0
• mul_zero (a : K) : a * 0 = 0
• mul_assoc (a b c : K) : a * b * c = a * (b * c)
• one : K
• one_mul (a : K) : 1 * a = a
• mul_one (a : K) : a * 1 = a
• natCast : ℕ → K
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → K → K
• npow_zero (x : K) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : K) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : K → K
• sub : K → K → K
• sub_eq_add_neg (a b : K) : a - b = a + -b
• zsmul : ℤ → K → K
• zsmul_zero' (a : K) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : K) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : K) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : K) : -a + a = 0
• intCast : ℤ → K
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• mul_comm (a b : K) : a * b = b * a
• inv : K → K
• div : K → K → K
• div_eq_mul_inv (a b : K) : a / b = a * b⁻¹
• zpow : ℤ → K → K
• zpow_zero' (a : K) : Field.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : K) : Field.zpow (↑n.succ) a = Field.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : K) : Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : K) (y : K), x ≠ y
• nnratCast : ℚ≥0 → K
• ratCast : ℚ → K
• mul_inv_cancel (a : K) : a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def (q : ℚ≥0) : ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → K → K
• nnqsmul_def (q : ℚ≥0) (a : K) : Field.nnqsmul q a = ↑q * a
• ratCast_def (q : ℚ) : ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → K → K
• qsmul_def (a : ℚ) (x : K) : Field.qsmul a x = ↑a * x
• dist : K → K → ℝ
• dist_self (x : K) : dist x x = 0
• dist_comm (x y : K) : dist x y = dist y x
• dist_triangle (x y z : K) : dist x z ≤ dist x y + dist y z
• edist : K → K → ENNReal
• edist_dist (x y : K) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace K
• uniformity_dist : uniformity K = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : K × K | dist p.1 p.2 < ε}
• toBornology : Bornology K
• cobounded_sets : (Bornology.cobounded K).sets = {s : Set K | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : K} : dist x y = 0 → x = y
• dist_eq (x y : K) : dist x y = ‖-x + y‖
• norm_mul (a b : K) : ‖a * b‖ = ‖a‖ * ‖b‖
• non_trivial : ∃ (x : K), 1 < ‖x‖
• locallyCompact : LocallyCompactSpace K

instance IsLocalField.properSpace (K : Type u_1) [IsLocalField K] : ProperSpace K

@[implicit_reducible]

noncomputable instance instIsLocalFieldReal : IsLocalField ℝ

@[implicit_reducible]

noncomputable instance instIsLocalFieldComplex : IsLocalField ℂ

@[implicit_reducible]

noncomputable instance instIsLocalFieldPadic (p : ℕ) [Fact (Nat.Prime p)] : IsLocalField ℚ_[p]

theorem isLocalField_iff_closedBalls_compact (K : Type u_1) [NontriviallyNormedField K] : LocallyCompactSpace K ↔ ∀ (x : K) (r : ℝ), IsCompact (Metric.closedBall x r)

theorem IsLocalField.completeSpace (K : Type u_1) [IsLocalField K] : CompleteSpace K

theorem isLocalField_iff_complete_dvr_finiteResidue {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] [Valued.v.RankOne] : ProperSpace K ↔ CompleteSpace K ∧ IsDiscreteValuationRing ↥(Valued.integer K) ∧ Finite (Valued.ResidueField K)

theorem isLocalField_iff_complete_finiteResidue_of_dvr {K : Type u_1} {Γ₀ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀] [Valued.v.RankOne] [IsDiscreteValuationRing ↥(Valued.integer K)] : ProperSpace K ↔ CompleteSpace K ∧ Finite (Valued.ResidueField K)

theorem locallyCompact_of_finiteDimensional_over_localField (K : Type u_1) [IsLocalField K] (L : Type u_2) [NontriviallyNormedField L] [NormedAlgebra K L] [FiniteDimensional K L] : LocallyCompactSpace L

@[reducible]

noncomputable def isLocalField_real : IsLocalField ℝ

@[reducible]

noncomputable def corollary_9_7_archimedean : IsLocalField ℝ

@[reducible]

noncomputable def isLocalField_padic (p : ℕ) [Fact (Nat.Prime p)] : IsLocalField ℚ_[p]

@[reducible]

noncomputable def corollary_9_7_padic (p : ℕ) [Fact (Nat.Prime p)] : IsLocalField ℚ_[p]

@[reducible]

noncomputable def isLocalField_of_finiteDimensional_extension (K : Type u_1) [IsLocalField K] (L : Type u_2) [NontriviallyNormedField L] [NormedAlgebra K L] [FiniteDimensional K L] : IsLocalField L

@[reducible]

noncomputable def corollary_9_7_finite_extension (K : Type u_1) [IsLocalField K] (L : Type u_2) [NontriviallyNormedField L] [NormedAlgebra K L] [FiniteDimensional K L] : IsLocalField L

@[reducible]

noncomputable def localField_Qp (p : ℕ) [Fact (Nat.Prime p)] : IsLocalField ℚ_[p]

@[reducible]

noncomputable def localField_R : IsLocalField ℝ

@[reducible]

noncomputable def localField_C : IsLocalField ℂ

theorem IsLocalField.finiteDimensional_of_locallyCompact_module (K : Type u_1) [IsLocalField K] {E : Type u_2} [AddCommGroup E] [UniformSpace E] [T2Space E] [IsUniformAddGroup E] [Module K E] [ContinuousSMul K E] [LocallyCompactSpace E] : FiniteDimensional K E

theorem not_accPt_of_separated {X : Type u_1} [MetricSpace X] {S : Set X} (h_sep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ dist x y) (a : X) : ¬AccPt a (Filter.principal S)

noncomputable def absValFromNorm (L : Type u_1) [NormedField L] [CharZero L] : AbsoluteValue ℚ ℝ

theorem absValFromNorm_isNontrivial (L : Type u_1) [IsLocalField L] [CharZero L] : (absValFromNorm L).IsNontrivial

noncomputable def normAbsValQ {L_v : Type u_1} [NontriviallyNormedField L_v] (j : ℚ →+* L_v) : AbsoluteValue ℚ ℝ

theorem absValFromNorm_eq_normAbsValQ_castHom (L : Type u_1) [NontriviallyNormedField L] [CharZero L] : absValFromNorm L = normAbsValQ (Rat.castHom L)

theorem normAbsValQ_isEquiv_real_uniformContinuous {L_v : Type u_1} [NontriviallyNormedField L_v] (j : ℚ →+* L_v) (hequiv : (normAbsValQ j).IsEquiv Rat.AbsoluteValue.real) : UniformContinuous ⇑j

noncomputable def extendRingHom_real {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (hequiv : (normAbsValQ j).IsEquiv Rat.AbsoluteValue.real) : ℝ →+* L_v

theorem extendRingHom_real_continuous {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (hequiv : (normAbsValQ j).IsEquiv Rat.AbsoluteValue.real) : Continuous ⇑(extendRingHom_real j hequiv)

theorem extendRingHom_real_extends {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (hequiv : (normAbsValQ j).IsEquiv Rat.AbsoluteValue.real) (q : ℚ) : (extendRingHom_real j hequiv) ↑q = j q

theorem normAbsValQ_isEquiv_padic_eq {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (hequiv : (normAbsValQ j).IsEquiv (Rat.AbsoluteValue.padic p)) (hnorm_p : ‖j ↑p‖ = (↑p)⁻¹) : normAbsValQ j = Rat.AbsoluteValue.padic p

theorem j_comp_equiv_continuous {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (heq : normAbsValQ j = Rat.AbsoluteValue.padic p) : Continuous ⇑(j.comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)

noncomputable def extendRingHom_padic {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (heq : normAbsValQ j = Rat.AbsoluteValue.padic p) : ℚ_[p] →+* L_v

theorem extendRingHom_padic_on_rat {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (heq : normAbsValQ j = Rat.AbsoluteValue.padic p) (q : ℚ) : (extendRingHom_padic j p heq) ↑q = j q

theorem extendRingHom_padic_continuous {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (heq : normAbsValQ j = Rat.AbsoluteValue.padic p) : Continuous ⇑(extendRingHom_padic j p heq)

theorem extendRingHom_padic_isometry {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (heq : normAbsValQ j = Rat.AbsoluteValue.padic p) (x : ℚ_[p]) : ‖(extendRingHom_padic j p heq) x‖ = ‖x‖

@[reducible]

noncomputable def completion_normedAlgebra_padic_of_eq (L_v : Type u_1) [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (heq : normAbsValQ j = Rat.AbsoluteValue.padic p) : NormedAlgebra ℚ_[p] L_v

@[reducible]

noncomputable def completion_normedAlgebra_padic (L_v : Type u_1) [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (hequiv : (normAbsValQ j).IsEquiv (Rat.AbsoluteValue.padic p)) (hnorm_p : ‖j ↑p‖ = (↑p)⁻¹) : NormedAlgebra ℚ_[p] L_v

theorem normAbsValQ_isEquiv_real_eq {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (hequiv : (normAbsValQ j).IsEquiv Rat.AbsoluteValue.real) (hnorm_2 : ‖j 2‖ = 2) : normAbsValQ j = Rat.AbsoluteValue.real

@[reducible]

noncomputable def completion_normedAlgebra_real_of_eq (L_v : Type u_1) [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (heq : normAbsValQ j = Rat.AbsoluteValue.real) : NormedAlgebra ℝ L_v

@[reducible]

noncomputable def completion_normedAlgebra_real (L_v : Type u_1) [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (hequiv : (normAbsValQ j).IsEquiv Rat.AbsoluteValue.real) (hnorm_2 : ‖j 2‖ = 2) : NormedAlgebra ℝ L_v

theorem j_comp_equiv_continuous_of_equiv {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (hequiv : (normAbsValQ j).IsEquiv (Rat.AbsoluteValue.padic p)) : Continuous ⇑(j.comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)

noncomputable def extendRingHom_padic_of_equiv {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (hequiv : (normAbsValQ j).IsEquiv (Rat.AbsoluteValue.padic p)) : ℚ_[p] →+* L_v

theorem extendRingHom_padic_of_equiv_continuous {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (p : ℕ) [Fact (Nat.Prime p)] (hequiv : (normAbsValQ j).IsEquiv (Rat.AbsoluteValue.padic p)) : Continuous ⇑(extendRingHom_padic_of_equiv j p hequiv)

noncomputable def localField_charZero_normedAlgebra_structure (L : Type u_1) [IsLocalField L] [CharZero L] : (x : Algebra ℝ L) ×' ContinuousSMul ℝ L ⊕ (p : ℕ) ×' (x : Fact (Nat.Prime p)) ×' (x_1 : Algebra ℚ_[p] L) ×' ContinuousSMul ℚ_[p] L

theorem localField_charZero_classification (L : Type u_1) [IsLocalField L] [CharZero L] : Nonempty (L ≃+* ℝ) ∨ Nonempty (L ≃+* ℂ) ∨ ∃ (p : ℕ) (x : Fact (Nat.Prime p)) (x_1 : Algebra ℚ_[p] L), FiniteDimensional ℚ_[p] L

theorem posChar_laurent_series_embedding (L : Type u_1) [IsLocalField L] (p : ℕ) [Fact (Nat.Prime p)] [CharP L p] : ∃ (n : ℕ) (_ : 0 < n) (f : LaurentSeries (GaloisField p n) →+* L), Function.Injective ⇑f

instance LaurentSeries.instIsRankOneDiscrete (K : Type u_1) [Field K] : Valued.v.IsRankOneDiscrete

@[reducible]

noncomputable instance LaurentSeries.instRankOne (K : Type u_1) [Field K] : Valued.v.RankOne

theorem posChar_continuousSMul_laurent_series (L : Type u_1) [inst_lf : IsLocalField L] (p : ℕ) [inst_p : Fact (Nat.Prime p)] [inst_cp : CharP L p] (n : ℕ) (hn : 0 < n) [inst_alg : Algebra (LaurentSeries (GaloisField p n)) L] (inst_nnf : NontriviallyNormedField (LaurentSeries (GaloisField p n))) : ContinuousSMul (LaurentSeries (GaloisField p n)) L

theorem posChar_finiteDimensional_over_laurent_series (L : Type u_1) [IsLocalField L] (p : ℕ) [Fact (Nat.Prime p)] [CharP L p] (n : ℕ) (hn : 0 < n) [Algebra (LaurentSeries (GaloisField p n)) L] : FiniteDimensional (LaurentSeries (GaloisField p n)) L

theorem localField_posChar_classification (L : Type u_1) [IsLocalField L] (p : ℕ) [Fact (Nat.Prime p)] [CharP L p] : ∃ (n : ℕ) (_ : 0 < n) (x : Algebra (LaurentSeries (GaloisField p n)) L), FiniteDimensional (LaurentSeries (GaloisField p n)) L

theorem localField_classification (L : Type u_1) [IsLocalField L] : Nonempty (L ≃+* ℝ) ∨ Nonempty (L ≃+* ℂ) ∨ (∃ (p : ℕ) (x : Fact (Nat.Prime p)) (x_1 : Algebra ℚ_[p] L), FiniteDimensional ℚ_[p] L) ∨ ∃ (p : ℕ) (x : Fact (Nat.Prime p)) (n : ℕ) (_ : 0 < n) (x_2 : Algebra (LaurentSeries (GaloisField p n)) L), FiniteDimensional (LaurentSeries (GaloisField p n)) L

@[implicit_reducible]

noncomputable instance NumberField.InfinitePlace.Completion.instIsLocalField {K : Type u_1} [Field K] (v : InfinitePlace K) : IsLocalField v.Completion

@[implicit_reducible]

noncomputable instance HeightOneSpectrum.adicCompletion.instIsLocalField {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : IsLocalField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

noncomputable def numberFieldCompletion_isLocalField {K : Type u_2} [Field K] [NumberField K] (v : NumberField.InfinitePlace K ⊕ IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : match v with | Sum.inl w => IsLocalField w.Completion | Sum.inr p => IsLocalField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K p)

noncomputable def corollary_9_7 {K : Type u_2} [Field K] [NumberField K] (v : NumberField.InfinitePlace K ⊕ IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : match v with | Sum.inl w => IsLocalField w.Completion | Sum.inr p => IsLocalField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K p)

@[reducible]

noncomputable def numberFieldCompletion_isLocalField_infinite {K : Type u_2} [Field K] [NumberField K] (v : NumberField.InfinitePlace K) : IsLocalField v.Completion

@[reducible]

noncomputable def corollary_9_7_infinite_place {K : Type u_2} [Field K] [NumberField K] (v : NumberField.InfinitePlace K) : IsLocalField v.Completion

@[reducible]

noncomputable def numberFieldCompletion_isLocalField_finite {K : Type u_2} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : IsLocalField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

@[reducible]

noncomputable def corollary_9_7_finite_place {K : Type u_2} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : IsLocalField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

theorem normAbsValQ_nontrivial {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] {L : Type u_2} [Field L] (hAlg : Algebra ℚ L) (hFD : FiniteDimensional ℚ L) (ι : L →+* L_v) (hdense : DenseRange ⇑ι) : (normAbsValQ (ι.comp (algebraMap ℚ L))).IsNontrivial

theorem completion_finiteDimensional_real (L_v : Type u_1) [NontriviallyNormedField L_v] [CompleteSpace L_v] (L : Type u_2) [Field L] (ι : L →+* L_v) (hdense : DenseRange ⇑ι) (hAlg : Algebra ℚ L) (hFD : FiniteDimensional ℚ L) (_hequiv : (normAbsValQ (ι.comp (algebraMap ℚ L))).IsEquiv Rat.AbsoluteValue.real) [inst : NormedAlgebra ℝ L_v] : FiniteDimensional ℝ L_v

theorem completion_finiteDimensional_padic (L_v : Type u_1) [NontriviallyNormedField L_v] [CompleteSpace L_v] (L : Type u_2) [Field L] (ι : L →+* L_v) (hdense : DenseRange ⇑ι) (hAlg : Algebra ℚ L) (hFD : FiniteDimensional ℚ L) (p : ℕ) [Fact (Nat.Prime p)] (_hequiv : (normAbsValQ (ι.comp (algebraMap ℚ L))).IsEquiv (Rat.AbsoluteValue.padic p)) [inst : NormedAlgebra ℚ_[p] L_v] : FiniteDimensional ℚ_[p] L_v

theorem properSpace_of_isCompact_closedBall_one {K : Type u_1} [NontriviallyNormedField K] (h : IsCompact (Metric.closedBall 0 1)) : ProperSpace K

theorem funcField_completion_closedUnitBall_compact (Fq : Type u_1) [Field Fq] [Fintype Fq] (L : Type u_2) [Field L] [Algebra (RatFunc Fq) L] [FiniteDimensional (RatFunc Fq) L] (L_v : Type u_3) [NontriviallyNormedField L_v] [CompleteSpace L_v] (ι : L →+* L_v) (hdense : DenseRange ⇑ι) : IsCompact (Metric.closedBall 0 1)

theorem completion_locallyCompact_functionField (Fq : Type u_1) [Field Fq] [Fintype Fq] (L : Type u_2) [Field L] [Algebra (RatFunc Fq) L] [FiniteDimensional (RatFunc Fq) L] (L_v : Type u_3) [NontriviallyNormedField L_v] [CompleteSpace L_v] (ι : L →+* L_v) (hdense : DenseRange ⇑ι) : LocallyCompactSpace L_v

@[reducible]

noncomputable def functionFieldCompletion_isLocalField (Fq : Type u_1) [Field Fq] [Fintype Fq] (L : Type u_2) [Field L] [Algebra (RatFunc Fq) L] [FiniteDimensional (RatFunc Fq) L] (L_v : Type u_3) [NontriviallyNormedField L_v] (hcompl : CompleteSpace L_v) (ι : L →+* L_v) (hdense : DenseRange ⇑ι) : IsLocalField L_v

@[reducible]

noncomputable def corollary_9_7_function_field (Fq : Type u_1) [Field Fq] [Fintype Fq] (L : Type u_2) [Field L] [Algebra (RatFunc Fq) L] [FiniteDimensional (RatFunc Fq) L] (L_v : Type u_3) [NontriviallyNormedField L_v] (hcompl : CompleteSpace L_v) (ι : L →+* L_v) (hdense : DenseRange ⇑ι) : IsLocalField L_v

theorem normAbsValQ_equiv_real_implies_eq {L_v : Type u_1} [NontriviallyNormedField L_v] [CompleteSpace L_v] (j : ℚ →+* L_v) (hequiv : (normAbsValQ j).IsEquiv Rat.AbsoluteValue.real) (hnorm_2 : ‖j 2‖ = 2) : normAbsValQ j = Rat.AbsoluteValue.real

theorem completion_padic_norm_p (L_v : Type u_1) [NontriviallyNormedField L_v] [CompleteSpace L_v] (L : Type u_2) [Field L] [hAlg : Algebra ℚ L] [hFD : FiniteDimensional ℚ L] (ι : L →+* L_v) (hdense : DenseRange ⇑ι) (p : ℕ) [Fact (Nat.Prime p)] (hpadic : (normAbsValQ (ι.comp (algebraMap ℚ L))).IsEquiv (Rat.AbsoluteValue.padic p)) : ‖(ι.comp (algebraMap ℚ L)) ↑p‖ = (↑p)⁻¹

theorem completion_arch_norm_two_of_equiv (L_v : Type u_1) [NontriviallyNormedField L_v] [CompleteSpace L_v] (L : Type u_2) [Field L] [hAlg : Algebra ℚ L] [hFD : FiniteDimensional ℚ L] (ι : L →+* L_v) (hdense : DenseRange ⇑ι) (hreal : (normAbsValQ (ι.comp (algebraMap ℚ L))).IsEquiv Rat.AbsoluteValue.real) : ‖(ι.comp (algebraMap ℚ L)) 2‖ = 2

@[reducible]

noncomputable def globalFieldCompletion_isLocalField (L_v : Type u_1) [NontriviallyNormedField L_v] [CompleteSpace L_v] (L : Type u_2) [Field L] (ι : L →+* L_v) (hdense : DenseRange ⇑ι) (hglobal : (∃ (x : Algebra ℚ L), FiniteDimensional ℚ L) ∨ ∃ (Fq : Type u_3) (x : Field Fq) (x_1 : Fintype Fq) (x_2 : Algebra (RatFunc Fq) L), FiniteDimensional (RatFunc Fq) L) : IsLocalField L_v

@[reducible]

noncomputable def corollary_9_7_global (L_v : Type u_1) [NontriviallyNormedField L_v] [CompleteSpace L_v] (L : Type u_2) [Field L] (ι : L →+* L_v) (hdense : DenseRange ⇑ι) (hglobal : (∃ (x : Algebra ℚ L), FiniteDimensional ℚ L) ∨ ∃ (Fq : Type u_3) (x : Field Fq) (x_1 : Fintype Fq) (x_2 : Algebra (RatFunc Fq) L), FiniteDimensional (RatFunc Fq) L) : IsLocalField L_v