spectralNorm_nonneg — Mathlib

English

K-algebra automorphisms of L preserve spectral norm: spectralNorm(K,L)(x) = spectralNorm(K,L)(σ x).

Русский

Автообразования K-алгебр L сохраняют спектральную норму: spectralNorm(K,L)(x) = spectralNorm(K,L)(σ x).

LaTeX

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

Lean4

/-- `spectralNorm K L y` is nonnegative. -/
theorem spectralNorm_nonneg (y : L) : 0 ≤ spectralNorm K L y :=
  le_ciSup_of_le (spectralValueTerms_bddAbove (minpoly K y)) 0 (spectralValueTerms_nonneg _ 0)

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