Commit 2021-12-09 16:26 94783bef

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}.