Theorems · Theorem · commutative algebra

spectralNorm_unique_of_finiteDimensional_normal

∀ (K : Type u_2) [inst : NormedField K] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hn : Normal K L] {f : AlgebraNorm K L},
  IsPowMul ⇑f →
    IsNonarchimedean ⇑f →
      (∀ (x : K), f ((algebraMap K L) x) = ↑‖x‖₊) →
        (∀ (σ : Gal(L/K)) (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.

Defined in

Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Cited by

0 results in Mathlib

Foundations

Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldFieldAlgebraFiniteDimensionalNormal