subset_circle_of_unitary — Mathlib

English

For a unitary element u in a C*-algebra, spectrum 𝕜 u ⊆ sphere 0 1, i.e., on the unit circle.

Русский

Для унитарного элемента u в C*-алгебре спектр 𝕜 u лежит на единичной окружности.

LaTeX

$$$$\operatorname{spectrum}_{\mathbb{C}}(u) \subseteq \{z \in \mathbb{C} : |z| = 1\}.$$$$

Lean4

theorem subset_circle_of_unitary {u : E} (h : u ∈ unitary E) : spectrum 𝕜 u ⊆ Metric.sphere 0 1 :=
  unitary.spectrum_subset_circle ⟨u, h⟩

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