Theorem IsStarNormal.spectralRadius_eq_nnnorm

Modification history

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