Theorems · Theorem · functional analysis

SpectrumRestricts.spectralRadius_eq

∀ {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} {A : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedRing A] [inst_3 : NormedAlgebra 𝕜₁ A] [inst_4 : NormedAlgebra 𝕜₂ A] [inst_5 : NormedAlgebra 𝕜₁ 𝕜₂]
  [IsScalarTower 𝕜₁ 𝕜₂ A] {f : 𝕜₂ → 𝕜₁} {a : A}, SpectrumRestricts a f → spectralRadius 𝕜₁ a = spectralRadius 𝕜₂ a

If 𝕜₁ is a normed field contained as subfield of a larger normed field 𝕜₂, and if a : A is an element whose 𝕜₂ spectrum restricts to 𝕜₁, then the spectral radii over each scalar field coincide.

Defined in

Mathlib.Analysis.Normed.Algebra.Spectrum

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedFieldNormedRingNormedAlgebraNormedAlgebraNormedAlgebraIsScalarTower