Theorems · Theorem · commutative algebra

spectralNorm.eq_of_normalClosure

∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L]
  {E : IntermediateField K L} {x : L} (g : ↥E),
  (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 the spectral norm of g : E when regarded as an element of the normal closure of E equals the spectral norm of x : L.

Defined in

Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedFieldFieldAlgebra