English
For suitable hA, if z lies in the spectrum of a, then algebraMapℂ→A(z) = a; i.e., the spectrum determines the preimage under the embedding.
Русский
При подходящих условиях hA, если z лежит в спектре a, то algebraMap_{ℂ→A}(z) = a; спектр полностью определяет прообраз через вложение.
LaTeX
$$$\\mathrm{algebraMap}_{\\mathbb{C} \\to A}(z) = a\\quad \\text{for } z \\in \\mathrm{spectrum}_{\\mathbb{C}}(a)\\,$ (under appropriate assumptions)$$
Lean4
/-- A specialization of the spectral mapping theorem for polynomials in a Banach algebra over `ℂ`
to monic monomials. -/
protected theorem map_pow (a : A) (n : ℕ) : spectrum ℂ (a ^ n) = (· ^ n) '' spectrum ℂ a := by
simpa only [aeval_X_pow, eval_X_pow] using map_polynomial_aeval a (X ^ n)
