Theorem resolventSet_neg

Modification history

2026-02-20 20:08
Mathlib/Algebra/Algebra/Spectrum/Basic.lean
feat(Algebra/Algebra/Spectrum/Basic): resolvent set of negative element (#35184) …
Added resolventSet_negView on Github →