mathlib documentation

analysis.normed_space.star.spectrum

Spectral properties in C⋆-algebras #

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

theorem unitary.spectrum_subset_circle {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [normed_algebra 𝕜 E] [complete_space E] [nontrivial E] (u : (unitary E)) :
theorem spectrum.subset_circle_of_unitary {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [normed_algebra 𝕜 E] [complete_space E] [nontrivial E] {u : E} (h : u unitary E) :
theorem self_adjoint.mem_spectrum_eq_re {A : Type u_1} [normed_ring A] [normed_algebra A] [complete_space A] [star_ring A] [cstar_ring A] [star_module A] [nontrivial A] {a : A} (ha : a self_adjoint A) {z : } (hz : z spectrum a) :
z = (z.re)

Any element of the spectrum of a selfadjoint is real.

Any element of the spectrum of a selfadjoint is real.

The spectrum of a selfadjoint is real

The spectrum of a selfadjoint is real