Theorems · Theorem · functional analysis

spectrum.map_pow

∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) (n : ℕ),
  spectrum ℂ (a ^ n) = (fun x => x ^ n) '' spectrum ℂ a

A specialization of the spectral mapping theorem for polynomials in a Banach algebra over ℂ to monic monomials.

Defined in

Mathlib.Analysis.Normed.Algebra.GelfandFormula

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedRingNormedAlgebraCompleteSpaceNontrivial