spectrum_eq — Mathlib

English

The spectrum of an element in a StarSubalgebra equals its spectrum in the ambient algebra.

Русский

Спектр элемента в StarSubalgebra равен спектру этого элемента в окружающей алгебре.

LaTeX

$$$$\operatorname{spectrum}_{\mathbb{C}}(a) = \operatorname{spectrum}_{\mathbb{C}}(a^{\,val}).$$$$

Lean4

/-- **Spectral permanence.** The spectrum of an element is invariant of the (closed)
`StarSubalgebra` in which it is contained. -/
theorem spectrum_eq {a : S} : spectrum ℂ a = spectrum ℂ (a : A) :=
  Set.ext fun _ ↦ S.mem_spectrum_iff

Похожие утверждения