The spectral norm and the norm extension theorem

This file shows that if K is a nonarchimedean normed field and L/K is an algebraic extension, then there is a natural extension of the norm on K to a K-algebra norm on L, the so-called spectral norm. The spectral norm of an element of L only depends on its minimal polynomial over K, so for K ⊆ L ⊆ M are two extensions of K, the spectral norm on M restricts to the spectral norm on L. This work can be used to uniquely extend the p-adic norm on ℚ_[p] to an algebraic closure of ℚ_[p], for example.

Details

We define the spectral value and the spectral norm. We prove the norm extension theorem [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Theorem 3.2.1/2)] [bosch-guntzer-remmert] : given a nonarchimedean normed field K and an algebraic extension L/K, the spectral norm is a power-multiplicative K-algebra norm on L extending the norm on K. All K-algebra automorphisms of L are isometries with respect to this norm. If L/K is finite, we get a formula relating the spectral norm on L with any other power-multiplicative norm on L extending the norm on K.

Moreover, we also prove the unique norm extension theorem: if K is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and L/K is an algebraic extension, then the spectral norm on L is a nonarchimedean multiplicative norm, and any power-multiplicative K-algebra norm on L coincides with the spectral norm. More over, if L/K is finite, then L is a complete space. This result is [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Theorem 3.2.4/2)][bosch-guntzer-remmert].

As a prerequisite, we formalize the proof of [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Proposition 3.1.2/1)][bosch-guntzer-remmert].

Main Definitions

• spectralValue : the spectral value of a polynomial in R[X].
• spectralNorm : the spectral norm |y|_sp is the spectral value of the minimal polynomial of y : L over K.
• spectralAlgNorm : the spectral norm is a K-algebra norm on L.
• spectralMulAlgNorm : the spectral norm is a multiplicative K-algebra norm on L.

Main Results

• norm_le_spectralNorm : if f is a power-multiplicative K-algebra norm on L, then f is bounded above by spectralNorm K L.
• spectralNorm_eq_of_equiv : the K-algebra automorphisms of L are isometries with respect to the spectral norm.
• spectralNorm_eq_iSup_of_finiteDimensional_normal : if L/K is finite and normal, then spectralNorm K L x = iSup (fun (σ : L ≃ₐ[K] L) ↦ f (σ x)).
• isPowMul_spectralNorm : the spectral norm is power-multiplicative.
• isNonarchimedean_spectralNorm : the spectral norm is nonarchimedean.
• spectralNorm_extends : the spectral norm extends the norm on K.
• spectralNorm_unique : any power-multiplicative K-algebra norm on L coincides with the spectral norm.
• spectralAlgNorm_mul : the spectral norm on L is multiplicative.
• spectralNorm.completeSpace : if L/K is finite dimensional, then L is a complete space with respect to topology induced by the spectral norm.

References

• [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert]

Tags

spectral, spectral norm, spectral value, seminorm, norm, nonarchimedean

def spectralValueTerms {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : ℕ → ℝ

The function ℕ → ℝ sending n to ‖ p.coeff n ‖^(1/(p.natDegree - n : ℝ)), if n < p.natDegree, or to 0 otherwise.

theorem spectralValueTerms_of_lt_natDegree {R : Type u_1} [SeminormedRing R] (p : Polynomial R) {n : ℕ} (hn : n < p.natDegree) : spectralValueTerms p n = ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))

theorem spectralValueTerms_of_natDegree_le {R : Type u_1} [SeminormedRing R] (p : Polynomial R) {n : ℕ} (hn : p.natDegree ≤ n) : spectralValueTerms p n = 0

def spectralValue {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : ℝ

The spectral value of a polynomial in R[X], where R is a seminormed ring. One motivation for the spectral value: if the norm on R is nonarchimedean, and if a monic polynomial splits into linear factors, then its spectral value is the norm of its largest root. See max_norm_root_eq_spectralValue.

theorem spectralValueTerms_finite_range {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : (Set.range (spectralValueTerms p)).Finite

The range of spectralValue_terms p is a finite set.

theorem spectralValueTerms_bddAbove {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : BddAbove (Set.range (spectralValueTerms p))

The sequence spectralValue_terms p is bounded above.

theorem spectralValueTerms_nonneg {R : Type u_1} [SeminormedRing R] (p : Polynomial R) (n : ℕ) : 0 ≤ spectralValueTerms p n

The sequence spectralValue_terms p is nonnegative.

theorem spectralValue_nonneg {R : Type u_1} [SeminormedRing R] (p : Polynomial R) : 0 ≤ spectralValue p

The spectral value of a polyomial is nonnegative.

theorem spectralValue_X_sub_C {R : Type u_1} [SeminormedRing R] [Nontrivial R] (r : R) : spectralValue (Polynomial.X - Polynomial.C r) = ‖r‖

The polynomial X - r has spectral value ‖ r ‖.

theorem spectralValue_X_pow {R : Type u_1} [SeminormedRing R] [Nontrivial R] (n : ℕ) : spectralValue (Polynomial.X ^ n) = 0

The polynomial X ^ n has spectral value 0.

theorem spectralValue_eq_zero_iff {R : Type u_1} [NormedRing R] [Nontrivial R] {p : Polynomial R} (hp : p.Monic) : spectralValue p = 0 ↔ p = Polynomial.X ^ p.natDegree

The spectral value of p equals zero if and only if p is of the form X ^ n.

theorem norm_root_le_spectralValue {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) {p : Polynomial K} (hp : p.Monic) {x : L} (hx : (Polynomial.aeval x) p = 0) : f x ≤ spectralValue p

The norm of any root of p is bounded by the spectral value of p. See [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Proposition 3.1.2/1(1))] [bosch-guntzer-remmert].

theorem max_norm_root_eq_spectralValue {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [DecidableEq L] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) (hf1 : f 1 = 1) (p : Polynomial K) (s : Multiset L) (hp : (Polynomial.mapAlg K L) p = (Multiset.map (fun (a : L) => Polynomial.X - Polynomial.C a) s).prod) : (⨆ (x : L), if x ∈ s then f x else 0) = spectralValue p

If f is a nonarchimedean, power-multiplicative K-algebra norm on L, then the spectral value of a polynomial p : K[X] that decomposes into linear factors in L is equal to the maximum of the norms of the roots. See [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis (Proposition 3.1.2/1(2))][bosch-guntzer-remmert].

def spectralNorm (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] (y : L) : ℝ

If L is an algebraic extension of a normed field K and y : L then the spectral norm spectralNorm K y : ℝ of y (written |y|_sp in the textbooks) is the spectral value of the minimal polynomial of y over K.

theorem spectralNorm.eq_of_tower {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {E : Type u_4} [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (x : E) : spectralNorm K E x = spectralNorm K L ((algebraMap E L) x)

If L/E/K is a tower of fields, then the spectral norm of x : E equals its spectral norm when regarding x as an element of L.

theorem spectralNorm.eq_of_normalClosure' {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] (E : IntermediateField K L) (x : ↥E) : spectralNorm K (↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) ((algebraMap ↥E ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) x) = spectralNorm K L ((algebraMap (↥E) L) x)

If L/E/K is a tower of fields, then the spectral norm of x : E when regarded as an element of the normal closure of E equals its spectral norm when regarding x as an element of L.

theorem spectralNorm.eq_of_normalClosure {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {E : IntermediateField K L} {x : L} (g : ↥E) (h_map : (algebraMap (↥E) L) g = x) : spectralNorm K (↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) ((algebraMap ↥E ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) g) = spectralNorm K L x

If L/E/K is a tower of fields and x = algebraMap E L g, then then the spectral norm of g : E when regarded as an element of the normal closure of E equals the spectral norm of x : L.

theorem spectralNorm_zero {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] : spectralNorm K L 0 = 0

spectralNorm K L (0 : L) = 0.

theorem spectralNorm_nonneg {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] (y : L) : 0 ≤ spectralNorm K L y

spectralNorm K L y is nonnegative.

theorem spectralNorm_zero_lt {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {y : L} (hy : y ≠ 0) (hy_alg : IsAlgebraic K y) : 0 < spectralNorm K L y

spectralNorm K L y is positive if y ≠ 0.

theorem eq_zero_of_map_spectralNorm_eq_zero {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {x : L} (hx : spectralNorm K L x = 0) (hx_alg : IsAlgebraic K x) : x = 0

If spectralNorm K L x = 0, then x = 0.

theorem norm_le_spectralNorm {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) {x : L} (hx_alg : IsAlgebraic K x) : f x ≤ spectralNorm K L x

If f is a power-multiplicative K-algebra norm on L, then f is bounded above by spectralNorm K L.

theorem spectralNorm_eq_of_equiv {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] (σ : L ≃ₐ[K] L) (x : L) : spectralNorm K L x = spectralNorm K L (σ x)

The K-algebra automorphisms of L are isometries with respect to the spectral norm.

theorem spectralNorm_eq_iSup_of_finiteDimensional_normal (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) (hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖) (x : L) : spectralNorm K L x = ⨆ (σ : L ≃ₐ[K] L), f (σ x)

If L/K is finite and normal, then spectralNorm K L x = supr (λ (σ : L ≃ₐ[K] L), f (σ x)).

theorem spectralNorm_eq_invariantExtension (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [hu : IsUltrametricDist K] : spectralNorm K L = ⇑(IsUltrametricDist.invariantExtension K L)

If L/K is finite and normal, then spectralNorm K L = invariantExtension K L.

theorem isPowMul_spectralNorm_of_finiteDimensional_normal (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] : IsPowMul (spectralNorm K L)

If L/K is finite and normal, then spectralNorm K L is power-multiplicative. See also the more general result isPowMul_spectralNorm.

def spectralAlgNorm_of_finiteDimensional_normal (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] : AlgebraNorm K L

The spectral norm is a K-algebra norm on L when L/K is finite and normal. See also spectralAlgNorm for a more general construction.

theorem spectralAlgNorm_of_finiteDimensional_normal_def (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] (x : L) : (spectralAlgNorm_of_finiteDimensional_normal K L) x = spectralNorm K L x

theorem isNonarchimedean_spectralNorm_of_finiteDimensional_normal (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] : IsNonarchimedean (spectralNorm K L)

The spectral norm is nonarchimedean when L/K is finite and normal. See also isNonarchimedean_spectralNorm for a more general result.

theorem spectralNorm_extends_of_finiteDimensional (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] [IsUltrametricDist K] (x : K) : spectralNorm K L ((algebraMap K L) x) = ‖x‖

The spectral norm extends the norm on K when L/K is finite and normal. See also spectralNorm_extends for a more general result.

theorem spectralNorm_unique_of_finiteDimensional_normal (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [h_fin : FiniteDimensional K L] [hn : Normal K L] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) (hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ↑‖x‖₊) (hf_iso : ∀ (σ : L ≃ₐ[K] L) (x : L), f x = f (σ x)) (x : L) : f x = spectralNorm K L x

If L/K is finite and normal, and f is a power-multiplicative K-algebra norm on L extending the norm on K, then f = spectralNorm K L.

instance instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] (E : IntermediateField K L) : SeminormClass (AlgebraNorm K ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))) K ↥(IntermediateField.normalClosure K (↥E) (AlgebraicClosure ↥E))

theorem spectralNorm_extends {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] (k : K) : spectralNorm K L ((algebraMap K L) k) = ‖k‖

The spectral norm extends the norm on K.

theorem spectralNorm_one {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] : spectralNorm K L 1 = 1

theorem spectralNorm_neg {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] {y : L} (hy : IsAlgebraic K y) : spectralNorm K L (-y) = spectralNorm K L y

spectralNorm K L (-y) = spectralNorm K L y .

theorem spectralNorm_smul {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] (k : K) {y : L} (hy : IsAlgebraic K y) : spectralNorm K L (k • y) = ↑‖k‖₊ * spectralNorm K L y

The spectral norm is compatible with the action of K.

theorem spectralNorm_mul {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] {x y : L} (hx : IsAlgebraic K x) (hy : IsAlgebraic K y) : spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y

The spectral norm is submultiplicative.

theorem isPowMul_spectralNorm {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] : IsPowMul (spectralNorm K L)

The spectral norm is power-multiplicative.

theorem isNonarchimedean_spectralNorm {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] : IsNonarchimedean (spectralNorm K L)

The spectral norm is nonarchimedean.

def spectralAlgNorm (K : Type u_2) [NormedField K] (L : Type u_3) [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] : AlgebraNorm K L

The spectral norm is a K-algebra norm on L.

theorem spectralAlgNorm_def {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] (x : L) : (spectralAlgNorm K L) x = spectralNorm K L x

theorem spectralAlgNorm_extends {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] (k : K) : (spectralAlgNorm K L) ((algebraMap K L) k) = ‖k‖

theorem spectralAlgNorm_one {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] : (spectralAlgNorm K L) 1 = 1

theorem spectralAlgNorm_isPowMul {K : Type u_2} [NormedField K] {L : Type u_3} [Field L] [Algebra K L] [IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] : IsPowMul ⇑(spectralAlgNorm K L)

theorem spectralNorm_unique {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsPowMul ⇑f) : f = spectralAlgNorm K L

If K is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and L/K is an algebraic extension, then any power-multiplicative K-algebra norm on L coincides with the spectral norm.

theorem spectralNorm_unique_field_norm_ext {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] {f : AbsoluteValue L ℝ} (hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖) (x : L) : f x = spectralNorm K L x

If K is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and L/K is an algebraic extension, then any multiplicative ring norm on L extending the norm on K coincides with the spectral norm.

def algNormFromConst {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] (h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1) {x : L} (hx : x ≠ 0) : AlgebraNorm K L

Given a nonzero x : L, and assuming that (spectralAlgNorm h_alg hna) 1 ≤ 1, this is the real-valued function sending y ∈ L to the limit of (f (y * x^n))/((f x)^n), regarded as an algebra norm.

theorem algNormFromConst_def {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] (h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1) {x y : L} (hx : x ≠ 0) : (algNormFromConst h1 hx) y = (seminormFromConst h1 ⋯ ⋯) y

theorem spectralAlgNorm_mul {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x y : L) : (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y

If K is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and L/K is an algebraic extension, then the spectral norm on L is multiplicative.

def spectralMulAlgNorm (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : MulAlgebraNorm K L

The spectral norm is a multiplicative K-algebra norm on L.

theorem spectralMulAlgNorm_def {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x : L) : (spectralMulAlgNorm K L) x = spectralNorm K L x

def spectralNorm.normedField (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : NormedField L

L with the spectral norm is a NormedField.

def spectralNorm.nontriviallyNormedField (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : NontriviallyNormedField L

L with the spectral norm is a NontriviallyNormedField.

def spectralNorm.normedAddCommGroup (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : NormedAddCommGroup L

L with the spectral norm is a normed_add_comm_group.

def spectralNorm.seminormedAddCommGroup (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : SeminormedAddCommGroup L

L with the spectral norm is a seminormed_add_comm_group.

def spectralNorm.normedSpace (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : NormedSpace K L

L with the spectral norm is a normed_space over K.

def spectralNorm.metricSpace (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : MetricSpace L

The metric space structure on L induced by the spectral norm.

def spectralNorm.uniformSpace (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] : UniformSpace L

The uniform space structure on L induced by the spectral norm.

@[instance 100]

instance spectralNorm.completeSpace (K : Type u) [NontriviallyNormedField K] (L : Type v) [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] [h_fin : FiniteDimensional K L] : CompleteSpace L

If L/K is finite dimensional, then L is a complete space with respect to topology induced by the spectral norm.