Theorems · Theorem · commutative algebra

spectralNorm.spectralNorm_eq_norm_coeff_zero_rpow

∀ (K : Type u) [inst : NontriviallyNormedField K] (L : Type v) [inst_1 : Field L] [inst_2 : Algebra K L]
  [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x : L),
  spectralNorm K L x = ‖(minpoly K x).coeff 0‖ ^ (1 / ↑(minpoly K x).natDegree)

For x : L with minimal polynomial f(X) := X^n + a_{n-1}X^{n-1} + ... + a_0 over K, the spectral norm of x is equal to ‖a_0‖^(1/(degree(f(X)))).

Defined in

Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldFieldAlgebraAlgebra.IsAlgebraicIsUltrametricDistCompleteSpace