mem_spectrum_iff — Mathlib

English

For a closed StarSubalgebra S of A, the spectrum of an element a ∈ S computed in S equals the spectrum computed in A.

Русский

Для элемента a ∈ S спектр в S совпадает со спектром в A.

LaTeX

$$$$\operatorname{spectrum}_{\mathbb{C}}(a) = \operatorname{spectrum}_{\mathbb{C}}(a : A).$$$$

Lean4

theorem mem_spectrum_iff {a : S} {z : ℂ} : z ∈ spectrum ℂ a ↔ z ∈ spectrum ℂ (a : A) :=
  not_iff_not.mpr S.coe_isUnit.symm

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