Theorems · Theorem · commutative algebra

spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots

∀ (K : Type u) [inst : NontriviallyNormedField K] (L : Type v) [inst_1 : Field L] [inst_2 : Algebra K L]
  [hu : IsUltrametricDist K] [inst_3 : CompleteSpace K] (x : L) {E : Type u_2} [inst_4 : Field E] [inst_5 : Algebra K E]
  [inst_6 : Algebra L E] [IsScalarTower K L E] [Polynomial.IsSplittingField L E ((Polynomial.mapAlg K L) (minpoly K x))]
  [inst_9 : Algebra.IsAlgebraic K E],
  (spectralMulAlgNorm K E) ((algebraMap L E) x) ^ (minpoly K x).natDegree =
    (spectralMulAlgNorm K E) ((Polynomial.mapAlg K E) (minpoly K x)).roots.prod

Given an algebraic tower of fields E/L/K and an element x : L whose minimal polynomial f over K splits into linear factors over E, the degree(f)th power of the spectral norm of x, considered as an element of E, is equal to the spectral norm of the product of the E-valued roots of f.

Defined in

Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldFieldAlgebraIsUltrametricDistCompleteSpaceFieldAlgebraAlgebraIsScalarTowerPolynomial.IsSplittingFieldAlgebra.IsAlgebraic