theorem NormedSpaceNorm.nullity {V : Type u_2} [NormedAddCommGroup V] (v : V) : ‖v‖ = 0 ↔ v = 0

theorem FiniteDimensionalNormTopology.complete (K : Type u_1) [NontriviallyNormedField K] [CompleteSpace K] (V : Type u_2) [NormedAddCommGroup V] [NormedSpace K V] [FiniteDimensional K V] : CompleteSpace V

theorem FiniteDimensionalNormTopology.linear_map_continuous (K : Type u_1) [NontriviallyNormedField K] [CompleteSpace K] {E : Type u_2} [AddCommGroup E] [Module K E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul K E] [T2Space E] [FiniteDimensional K E] {F : Type u_3} [AddCommGroup F] [Module K F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul K F] (f : E →ₗ[K] F) : Continuous ⇑f

theorem FiniteDimensionalNormTopology.completeSpace_and_continuous_linearMap (K : Type u_1) [NontriviallyNormedField K] [CompleteSpace K] : (∀ (V : Type u_2) [inst : NormedAddCommGroup V] [inst_1 : NormedSpace K V] [FiniteDimensional K V], CompleteSpace V) ∧ ∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module K E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul K E] [T2Space E] [FiniteDimensional K E] {F : Type u_4} [inst_7 : AddCommGroup F] [inst_8 : Module K F] [inst_9 : TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul K F] (f : E →ₗ[K] F), Continuous ⇑f

theorem integralClosure_completeDVR_isDVR (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra A L] [IsScalarTower A K L] (B : Type u_4) [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] : IsDiscreteValuationRing B

instance AbsoluteValueExtension.algebraIsAlgebraic (K : Type u_1) [NontriviallyNormedField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] : Algebra.IsAlgebraic K L

theorem AbsoluteValueExtension.spectralNorm_extends_norm (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] (k : K) : spectralNorm K L ((algebraMap K L) k) = ‖k‖

theorem AbsoluteValueExtension.spectralNorm_unique_extension (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] (f : AbsoluteValue L ℝ) (hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖) (x : L) : f x = spectralNorm K L x

theorem AbsoluteValueExtension.finiteExtension_completeSpace (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] : CompleteSpace L

theorem AbsoluteValueExtension.spectralNorm_le_one_iff_minpoly_coeff_norm_le_one (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] (x : L) : spectralNorm K L x ≤ 1 ↔ ∀ (i : ℕ), ‖(minpoly K x).coeff i‖ ≤ 1

theorem AbsoluteValueExtension.integralClosure_isDVR (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (A : Type u_3) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] (B : Type u_4) [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] : IsDiscreteValuationRing B

theorem AbsoluteValueExtension.norm_algebraMap_unit_eq_one {R : Type u_3} [CommRing R] [IsDomain R] {F : Type u_4} [NormedField F] [Algebra R F] [IsFractionRing R F] (hbdd : ∀ (r : R), ‖(algebraMap R F) r‖ ≤ 1) {x : R} (hu : IsUnit x) : ‖(algebraMap R F) x‖ = 1

theorem AbsoluteValueExtension.dvd_pow_of_norm_le_pow {R : Type u_3} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {F : Type u_4} [NormedField F] [Algebra R F] [IsFractionRing R F] (hbdd : ∀ (r : R), ‖(algebraMap R F) r‖ ≤ 1) (hnu : ∀ (r : R), ¬IsUnit r → ‖(algebraMap R F) r‖ < 1) {π : R} (hπ : Irreducible π) (x : R) (n : ℕ) (hx : ‖(algebraMap R F) x‖ ≤ ‖(algebraMap R F) π‖ ^ n) : π ^ n ∣ x

theorem AbsoluteValueExtension.isPrecomplete_maximalIdeal_of_completeSpace_fractionField (F : Type u_3) [NormedField F] [CompleteSpace F] (R : Type u_4) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Algebra R F] [IsFractionRing R F] (hbdd : ∀ (r : R), ‖(algebraMap R F) r‖ ≤ 1) (hnu : ∀ (r : R), ¬IsUnit r → ‖(algebraMap R F) r‖ < 1) (hbdd_surj : ∀ (x : F), ‖x‖ ≤ 1 → ∃ (r : R), (algebraMap R F) r = x) : IsPrecomplete (IsLocalRing.maximalIdeal R) R

theorem AbsoluteValueExtension.norm_algebraMap_dvr_le_one (A : Type u_3) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_4) [NontriviallyNormedField K] [IsUltrametricDist K] [Algebra A K] [IsFractionRing A K] (a : A) : ‖(algebraMap A K) a‖ ≤ 1

theorem AbsoluteValueExtension.spectralNorm_algebraMap_le_one (K : Type u_3) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] (B : Type u_6) [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] (r : B) : ‖(algebraMap B L) r‖ ≤ 1

theorem AbsoluteValueExtension.monic_irreducible_coeff_norm_le_one_lifts_to_DVR (K : Type u_3) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (A : Type u_4) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Algebra A K] [IsFractionRing A K] (f : Polynomial K) (hf_monic : f.Monic) (hf_irr : Irreducible f) (hcoeff : ∀ (i : ℕ), ‖f.coeff i‖ ≤ 1) : ∃ (g : Polynomial A), Polynomial.map (algebraMap A K) g = f

theorem AbsoluteValueExtension.spectralNorm_le_one_of_mem (K : Type u_3) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] (B : Type u_6) [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] (x : L) (hx : ‖x‖ ≤ 1) : ∃ (r : B), (algebraMap B L) r = x

theorem AbsoluteValueExtension.spectralNorm_nonunit_lt_one (K : Type u_3) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] (B : Type u_6) [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsDiscreteValuationRing B] (r : B) (hr : ¬IsUnit r) : ‖(algebraMap B L) r‖ < 1

theorem AbsoluteValueExtension.isPrecomplete_integralClosure_of_completeSpace (K : Type u_3) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] (B : Type u_6) [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsDiscreteValuationRing B] : IsPrecomplete (IsLocalRing.maximalIdeal B) B

theorem AbsoluteValueExtension.integralClosure_isAdicComplete (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (A : Type u_3) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] (B : Type u_4) [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [hDVR : IsDiscreteValuationRing B] : IsAdicComplete (IsLocalRing.maximalIdeal B) B

theorem AbsoluteValueExtension.spectralNorm_extension_exists_unique (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] : (∀ (k : K), spectralNorm K L ((algebraMap K L) k) = ‖k‖) ∧ ∀ (f : AbsoluteValue L ℝ), (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) → ∀ (x : L), f x = spectralNorm K L x

theorem AbsoluteValueExtension.finiteExtension_complete_and_valuation_ring (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] : CompleteSpace L ∧ ∀ (x : L), spectralNorm K L x ≤ 1 ↔ ∀ (i : ℕ), ‖(minpoly K x).coeff i‖ ≤ 1

theorem AbsoluteValueExtension.spectralNorm_unique_complete_integralClosure_isDVR (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] (A : Type u_3) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] (B : Type u_4) [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] : ((∀ (k : K), spectralNorm K L ((algebraMap K L) k) = ‖k‖) ∧ ∀ (f : AbsoluteValue L ℝ), (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) → ∀ (x : L), f x = spectralNorm K L x) ∧ (CompleteSpace L ∧ ∀ (x : L), spectralNorm K L x ≤ 1 ↔ ∀ (i : ℕ), ‖(minpoly K x).coeff i‖ ≤ 1) ∧ (Algebra.IsSeparable K L → ∃ (hDVR : IsDiscreteValuationRing B), IsAdicComplete (IsLocalRing.maximalIdeal B) B)

theorem ValuationFormula.val_one {L : Type u_1} [Field L] (v : L → ℤ) (hv : ∀ (a b : L), a ≠ 0 → b ≠ 0 → v (a * b) = v a + v b) : v 1 = 0

theorem ValuationFormula.val_inv {L : Type u_1} [Field L] (v : L → ℤ) (hv : ∀ (a b : L), a ≠ 0 → b ≠ 0 → v (a * b) = v a + v b) (a : L) (ha : a ≠ 0) : v a⁻¹ = -v a

theorem ValuationFormula.val_pow_nat {L : Type u_1} [Field L] (v : L → ℤ) (hv : ∀ (a b : L), a ≠ 0 → b ≠ 0 → v (a * b) = v a + v b) (a : L) (ha : a ≠ 0) (n : ℕ) : v (a ^ n) = ↑n * v a

theorem ValuationFormula.val_zpow {L : Type u_1} [Field L] (v : L → ℤ) (hv : ∀ (a b : L), a ≠ 0 → b ≠ 0 → v (a * b) = v a + v b) (a : L) (ha : a ≠ 0) (n : ℤ) : v (a ^ n) = n * v a

theorem ValuationFormula.norm_zpow {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [FiniteDimensional K L] (x : L) (n : ℤ) : (Algebra.norm K) (x ^ n) = (Algebra.norm K) x ^ n

theorem ValuationFormula.dvr_norm_decomp {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [FiniteDimensional K L] (v_K : K → ℤ) (v_L : L → ℤ) (π_L : L) (hv_K : ∀ (a b : K), a ≠ 0 → b ≠ 0 → v_K (a * b) = v_K a + v_K b) (hv_L : ∀ (a b : L), a ≠ 0 → b ≠ 0 → v_L (a * b) = v_L a + v_L b) (hπ_L : π_L ≠ 0) (hπ_L_val : v_L π_L = 1) (x : L) (hx : x ≠ 0) : ∃ (u : L), u ≠ 0 ∧ v_L u = 0 ∧ v_K ((Algebra.norm K) x) = v_K ((Algebra.norm K) u) + v_L x * v_K ((Algebra.norm K) π_L)

theorem ValuationFormula.norm_valuation_identity {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [FiniteDimensional K L] (v_K : K → ℤ) (v_L : L → ℤ) (π_L : L) (f_q : ℕ) (hv_K : ∀ (a b : K), a ≠ 0 → b ≠ 0 → v_K (a * b) = v_K a + v_K b) (hv_L : ∀ (a b : L), a ≠ 0 → b ≠ 0 → v_L (a * b) = v_L a + v_L b) (_hf_q : 0 < f_q) (hπ_L : π_L ≠ 0) (hπ_L_val : v_L π_L = 1) (h_unif_norm : v_K ((Algebra.norm K) π_L) = ↑f_q) (h_unit_norm : ∀ (u : L), u ≠ 0 → v_L u = 0 → v_K ((Algebra.norm K) u) = 0) (x : L) (hx : x ≠ 0) : v_K ((Algebra.norm K) x) = ↑f_q * v_L x

theorem ValuationFormula.valuation_formula {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [FiniteDimensional K L] (v_K : K → ℤ) (v_L : L → ℤ) (π_L : L) (f_q : ℕ) (hv_K : ∀ (a b : K), a ≠ 0 → b ≠ 0 → v_K (a * b) = v_K a + v_K b) (hv_L : ∀ (a b : L), a ≠ 0 → b ≠ 0 → v_L (a * b) = v_L a + v_L b) (hf_q : 0 < f_q) (hπ_L : π_L ≠ 0) (hπ_L_val : v_L π_L = 1) (h_unif_norm : v_K ((Algebra.norm K) π_L) = ↑f_q) (h_unit_norm : ∀ (u : L), u ≠ 0 → v_L u = 0 → v_K ((Algebra.norm K) u) = 0) (x : L) (hx : x ≠ 0) : ↑(v_L x) = 1 / ↑f_q * ↑(v_K ((Algebra.norm K) x))

theorem valuation_eq_inv_residueDeg_mul_norm_valuation {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [FiniteDimensional K L] (v_K : K → ℤ) (v_L : L → ℤ) (π_L : L) (f_q : ℕ) (hv_K : ∀ (a b : K), a ≠ 0 → b ≠ 0 → v_K (a * b) = v_K a + v_K b) (hv_L : ∀ (a b : L), a ≠ 0 → b ≠ 0 → v_L (a * b) = v_L a + v_L b) (hf_q : 0 < f_q) (hπ_L : π_L ≠ 0) (hπ_L_val : v_L π_L = 1) (h_unif_norm : v_K ((Algebra.norm K) π_L) = ↑f_q) (h_unit_norm : ∀ (u : L), u ≠ 0 → v_L u = 0 → v_K ((Algebra.norm K) u) = 0) (x : L) (hx : x ≠ 0) : ↑(v_L x) = 1 / ↑f_q * ↑(v_K ((Algebra.norm K) x))