English
If L/K is finite and normal, then spectralValue(p) equals the supremum of f(σ x) over all automorphisms σ of L over K, for a suitable norm f.
Русский
Если L/K конечное и нормальное, спектральное значение полинома равняется супремусу f(σ x) по всем автообразованиям σ над K.
LaTeX
$$$$\operatorname{spectralValue}(p)=\sup_{\sigma\in \operatorname{Aut}_K(L)} f(\sigma x).$$$$
Lean4
/-- 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 eq_of_normalClosure' (x : E) :
spectralNorm K (normalClosure K E (AlgebraicClosure E)) (algebraMap E (normalClosure K E (AlgebraicClosure E)) x) =
spectralNorm K L (algebraMap E L x) :=
by
simp only [spectralNorm, spectralValue]
have h_min :
minpoly K (algebraMap (↥E) (↥(normalClosure K (↥E) (AlgebraicClosure ↥E))) x) = minpoly K (algebraMap (↥E) L x) :=
by
rw [minpoly.algebraMap_eq (algebraMap (↥E) ↥(normalClosure K E (AlgebraicClosure E))).injective x, ←
minpoly.algebraMap_eq (algebraMap (↥E) L).injective x]
simp_rw [h_min]
