# Conditions on unitary elements imposed by the continuous functional calculus #

## Main theorems #

`unitary_iff_isStarNormal_and_spectrum_subset_unitary`

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

theorem
cfc_unitary_iff
{R : Type u_1}
{A : Type u_2}
{p : A → Prop}
[CommRing R]
[StarRing R]
[MetricSpace R]
[TopologicalRing R]
[ContinuousStar R]
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra R A]
[ContinuousFunctionalCalculus R p]
(f : R → R)
(a : A)
(ha : autoParam (p a) _auto✝)
(hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝)
:

theorem
unitary_iff_isStarNormal_and_spectrum_subset_unitary
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
{u : A}
:

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