# Documentation

Mathlib.Analysis.NormedSpace.Star.Spectrum

# Spectral properties in C⋆-algebras #

In this file, we establish various properties related to the spectrum of elements in C⋆-algebras.

theorem unitary.spectrum_subset_circle {𝕜 : Type u_1} [] {E : Type u_2} [] [] [] [] [] (u : { x // x }) :
spectrum 𝕜 u
theorem spectrum.subset_circle_of_unitary {𝕜 : Type u_1} [] {E : Type u_2} [] [] [] [] [] {u : E} (h : u ) :
spectrum 𝕜 u
theorem IsSelfAdjoint.spectralRadius_eq_nnnorm {A : Type u_1} [] [] [] [] [] {a : A} (ha : ) :
theorem IsStarNormal.spectralRadius_eq_nnnorm {A : Type u_1} [] [] [] [] [] (a : A) [] :
theorem IsSelfAdjoint.mem_spectrum_eq_re {A : Type u_1} [] [] [] [] [] [] {a : A} (ha : ) {z : } (hz : z ) :
z = z.re

Any element of the spectrum of a selfadjoint is real.

theorem selfAdjoint.mem_spectrum_eq_re {A : Type u_1} [] [] [] [] [] [] (a : { x // x }) {z : } (hz : z ) :
z = z.re

Any element of the spectrum of a selfadjoint is real.

theorem IsSelfAdjoint.val_re_map_spectrum {A : Type u_1} [] [] [] [] [] [] {a : A} (ha : ) :

The spectrum of a selfadjoint is real

theorem selfAdjoint.val_re_map_spectrum {A : Type u_1} [] [] [] [] [] [] (a : { x // x }) :
=

The spectrum of a selfadjoint is real

theorem StarAlgHom.nnnorm_apply_le {F : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [] [] [] [] [] [] [hF : ] (φ : F) (a : A) :

A star algebra homomorphism of complex C⋆-algebras is norm contractive.

theorem StarAlgHom.norm_apply_le {F : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [] [] [] [] [] [] [hF : ] (φ : F) (a : A) :
φ a a

A star algebra homomorphism of complex C⋆-algebras is norm contractive.

Star algebra homomorphisms between C⋆-algebras are continuous linear maps. See note [lower instance priority]

noncomputable instance WeakDual.Complex.instStarHomClass {F : Type u_1} {A : Type u_2} [] [] [] [] [] [] [hF : ] :

This instance is provided instead of StarAlgHomClass to avoid type class inference loops. See note [lower instance priority]

noncomputable def AlgHomClass.instStarAlgHomClass {F : Type u_1} {A : Type u_2} [] [] [] [] [] [] [hF : ] :

This is not an instance to avoid type class inference loops. See WeakDual.Complex.instStarHomClass.

Instances For
noncomputable instance WeakDual.CharacterSpace.instStarAlgHomClass {A : Type u_2} [] [] [] [] [] [] :