Theorem IsIdempotentElem.quasispectrum_subset

Modification history

2026-03-10 21:33
Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
feat(Analysis/CStarAlgebra): `IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1}` (#35916) …
Modified IsIdempotentElem.quasispectrum_subsetView on Github →
2025-07-26 16:23
Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
feat(Analysis/CStarAlgebra/...): an idempotent element in a C*-algebra is self-adjoint iff it is normal (#27475)
Added IsIdempotentElem.quasispectrum_subsetView on Github →