Mathlib v3 is deprecated. Go to Mathlib v4

Theorem spectrum.norm_resolvent_le_forall

Modification history

2022-03-01 17:25

src/analysis/normed_space/spectrum.lean

feat(algebra/algebra/spectrum, analysis/normed_space/spectrum): prove the spectrum of any element in a complex Banach algebra is nonempty (#12115) …

Added spectrum.norm_resolvent_le_forall View on Github →