Theorem IsSelfAdjoint.im_eq_zero_of_mem_spectrum

Modification history

2024-08-16 23:11
Mathlib/Analysis/CStarAlgebra/Spectrum.lean
feat: better proof of spectral permanence (#15603) …
Added IsSelfAdjoint.im_eq_zero_of_mem_spectrumView on Github →