Documentation

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary

Conditions on unitary elements imposed by the continuous functional calculus #

Main theorems #

theorem cfc_unitary_iff {R : Type u_1} {A : Type u_2} {p : AProp} [CommRing R] [StarRing R] [MetricSpace R] [TopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p] (f : RR) (a : A) (ha : autoParam (p a) _auto✝) (hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝) :
cfc f a unitary A xspectrum R a, star (f x) * f x = 1