Commit 2022-10-27 20:17 11dcb6b5

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.