mathlib3

94783bef - feat(algebra/algebra/spectrum): lemmas when scalars are a field (#10476)

feat(algebra/algebra/spectrum): lemmas when scalars are a field (#10476) Prove some properties of the spectrum when the underlying scalar ring is a field, and mostly assuming the algebra is itself nontrivial. Show that the spectrum of a scalar (i.e., `algebra_map 𝕜 A k`) is the singleton `{k}`. Prove that `σ (a * b) \ {0} = σ (b * a) \ {0}`.