Commit 2026-02-20 20:08 eeb0516d

View on Github →

feat(Algebra/Algebra/Spectrum/Basic): resolvent set of negative element (#35184) This PR adds a basic API lemma resolventSet_neg stating that resolventSet R (-a) = -resolventSet R a.

Estimated changes

added theorem resolventSet_neg
modified theorem spectrum.neg_eq