mathlib

f684f612 - feat(algebra/algebra/spectrum): define spectrum and prove basic prope... (#10390)

feat(algebra/algebra/spectrum): define spectrum and prove basic prope... (#10390) …rties Define the resolvent set and the spectrum of an element of an algebra as a set of elements in the scalar ring. We prove a few basic facts including that additive cosets of the spectrum commute with the spectrum, that is, r + σ a = σ (r ⬝ 1 + a). Similarly, multiplicative cosets of the spectrum also commute when the element r is a unit of the scalar ring R. Finally, we also show that the units of R in σ (a*b) coincide with those of σ (b*a).