Theorem unitary.spectrum_subset_circle

Modification history

2023-06-11 15:21
Mathlib/Analysis/NormedSpace/Star/Spectrum.lean
feat: port Analysis.NormedSpace.Star.Spectrum (#4964) …
Added unitary.spectrum_subset_circleView on Github →