English
For a power-multiplicative norm f on L that is nonarchimedean, and for algebraic x, f(x) ≤ spectralValue(p) where p is the minimal polynomial of x over K.
Русский
Для нормы f на L, удовлетворяющей свойствам умножения и неархимедовой, и для алгебраического x, выполняется f(x) ≤ spectralValue(p), где p — минимальный полином x над K.
LaTeX
$$$$f(x) \le \operatorname{spectralValue}(p).$$$$
Lean4
/-- If `f` is a power-multiplicative `K`-algebra norm on `L`, then `f`
is bounded above by `spectralNorm K L`. -/
theorem norm_le_spectralNorm {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 :=
norm_root_le_spectralValue hf_pm hf_na (minpoly.monic hx_alg.isIntegral) (by rw [minpoly.aeval])
