Conditions on unitary elements imposed by the continuous functional calculus

Main theorems

• unitary_iff_isStarNormal_and_spectrum_subset_circle: An element is unitary if and only if it is star-normal and its spectrum lies on the unit circle.

theorem unitary_iff_isStarNormal_and_spectrum_subset_circle {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] {u : A} : u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ ↑circle

theorem mem_unitary_of_spectrum_subset_circle {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] {u : A} [IsStarNormal u] (hu : spectrum ℂ u ⊆ ↑circle) : u ∈ unitary A

theorem spectrum_subset_circle_of_mem_unitary {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ IsStarNormal] {u : A} (hu : u ∈ unitary A) : spectrum ℂ u ⊆ ↑circle