Theorem QuasispectrumRestricts.nnreal_of_nonneg

Modification history

2025-10-09 08:14

Mathlib/Analysis/Normed/Algebra/Spectrum.lean

chore: move some results from `Analysis/Normed/Algebra/Spectrum` to `Analysis/{Real, Complex}/Spectrum` (#29916)

Modified QuasispectrumRestricts.nnreal_of_nonneg View on Github →

2024-05-13 12:50

Mathlib/Analysis/NormedSpace/Spectrum.lean

refactor: generalize `SpectrumRestricts` to the `QuasispectrumRestricts`, preserving API (#12643)

Added QuasispectrumRestricts.nnreal_of_nonneg View on Github →