Theorem IsIdempotentElem.finite_quasispectrum

Modification history

2026-03-10 21:33
Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
feat(Analysis/CStarAlgebra): `IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1}` (#35916) …
Added IsIdempotentElem.finite_quasispectrumView on Github →