Mathlib Changelog
v4
Changelog
About
Github
Theorem
spectrum.subset_circle_of_unitary
Modification history
2023-06-11 15:21
Mathlib/Analysis/NormedSpace/Star/Spectrum.lean
feat: port Analysis.NormedSpace.Star.Spectrum (#4964) …
Added
spectrum.subset_circle_of_unitary
View on Github →