eq_of_normalClosure — Mathlib

English

If L/K is finite and normal, the spectral norm equals the invariant extension norm.

Русский

Если L/K конечное и нормальное, спектральная норма совпадает с нормой инвариантного расширения.

LaTeX

$$$$\operatorname{spectralNorm}(K,L)=\operatorname{invariantExtension}(K,L).$$$$

Lean4

/-- 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`. -/
theorem eq_of_normalClosure {E : IntermediateField K L} {x : L} (g : E) (h_map : algebraMap E L g = x) :
    spectralNorm K (normalClosure K E (AlgebraicClosure E)) (algebraMap E (normalClosure K E (AlgebraicClosure E)) g) =
      spectralNorm K L x :=
  h_map ▸ spectralNorm.eq_of_normalClosure' E g

Похожие утверждения