noncomputable def Polynomial.L1norm {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (f : Polynomial K) : ℝ

theorem Polynomial.L1norm_def {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (f : Polynomial K) : L1norm v f = ∑ i ∈ f.support, v (f.coeff i)

@[simp]

theorem Polynomial.L1norm_zero {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : L1norm v 0 = 0

theorem Polynomial.L1norm_nonneg {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (f : Polynomial K) : 0 ≤ L1norm v f

theorem Polynomial.L1norm_eq_sum_range {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (f : Polynomial K) : L1norm v f = ∑ i ∈ Finset.range (f.natDegree + 1), v (f.coeff i)

theorem Polynomial.L1norm_monic_eq {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (f : Polynomial K) (hf : f.Monic) : L1norm v f = ∑ i ∈ Finset.range f.natDegree, v (f.coeff i) + 1

theorem Polynomial.L1norm_monic_ge_one {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (f : Polynomial K) (hf : f.Monic) : 1 ≤ L1norm v f

theorem Polynomial.root_norm_lt_L1norm {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (f : Polynomial K) {L : Type u_2} [Field L] [Algebra K L] (w : AbsoluteValue L ℝ) (hcompat : ∀ (k : K), w ((algebraMap K L) k) = v k) (hf : f.Monic) {α : L} (hα : (aeval α) f = 0) : w α < L1norm v f

theorem automorphism_preserves_spectralNorm {K : Type u_1} [NormedField K] {L : Type u_2} [Field L] [Algebra K L] (σ : Gal(L/K)) (α : L) : spectralNorm K L (σ α) = spectralNorm K L α

@[deprecated automorphism_preserves_spectralNorm (since := "2026-05-04")]

theorem Lemma_11_13 (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (σ : Gal(AlgebraicClosure K/K)) (α : AlgebraicClosure K) : spectralNorm K (AlgebraicClosure K) (σ α) = spectralNorm K (AlgebraicClosure K) α

def BelongsTo (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (β α : AlgebraicClosure K) : Prop

theorem krasner_lemma (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {α β : AlgebraicClosure K} (hsep : IsSeparable K α) (hbelong : BelongsTo K β α) : K⟮α⟯ ≤ K⟮β⟯

@[deprecated krasner_lemma (since := "2026-05-04")]

theorem Lemma_11_15 (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {α β : AlgebraicClosure K} (hsep : IsSeparable K α) (hbelong : BelongsTo K β α) : K⟮α⟯ ≤ K⟮β⟯

theorem multiset_prod_ge_pow_of_nonneg_ge {s : Multiset ℝ} {c : ℝ} (hc : 0 ≤ c) (hnonneg : ∀ x ∈ s, 0 ≤ x) (hge : ∀ x ∈ s, c ≤ x) : c ^ s.card ≤ s.prod

noncomputable def normAbsVal (K : Type u_1) [NormedField K] : AbsoluteValue K ℝ

theorem continuity_of_roots (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (f : Polynomial K) (hf_monic : f.Monic) (hf_irr : Irreducible f) (hf_sep : f.Separable) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (g : Polynomial K), g.Monic → g.natDegree = f.natDegree → Polynomial.L1norm (normAbsVal K) (f - g) < δ → ∀ (β : AlgebraicClosure K), (Polynomial.aeval β) g = 0 → ∃ (α : AlgebraicClosure K), (Polynomial.aeval α) f = 0 ∧ BelongsTo K β α ∧ K⟮α⟯ = K⟮β⟯

theorem Multiset.eq_of_mem_of_mem_of_card_le_one {α : Type u_1} [DecidableEq α] {s : Multiset α} {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : s.card ≤ 1) : a = b

@[deprecated continuity_of_roots (since := "2026-05-04")]

theorem Theorem_11_19 (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (f : Polynomial K) (hf_monic : f.Monic) (hf_irr : Irreducible f) (hf_sep : f.Separable) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (g : Polynomial K), g.Monic → g.natDegree = f.natDegree → Polynomial.L1norm (normAbsVal K) (f - g) < δ → ∀ (β : AlgebraicClosure K), (Polynomial.aeval β) g = 0 → ∃ (α : AlgebraicClosure K), (Polynomial.aeval α) f = 0 ∧ BelongsTo K β α ∧ K⟮α⟯ = K⟮β⟯

theorem continuity_of_roots_irreducible_separable (K : Type u_1) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] (f : Polynomial K) (hf_monic : f.Monic) (hf_irr : Irreducible f) (hf_sep : f.Separable) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (g : Polynomial K), g.Monic → g.natDegree = f.natDegree → Polynomial.L1norm (normAbsVal K) (f - g) < δ → Irreducible g ∧ g.Separable