mathlib

11dcb6b5 - feat(algebra/algebra/spectrum): add a few basic lemmas for convenience (#17156)

feat(algebra/algebra/spectrum): add a few basic lemmas for convenience (#17156) This adds a few basic lemmas concerning the spectrum of an element which are particularly convenient and were missing. In addiiton, we golf a few existing declarations and otherwise try to clean up the file a bit.