Commit 2026-03-10 21:33 b0b8870e

View on Github →

feat(Analysis/CStarAlgebra): IsIdempotentElem a ↔ spectrum R a ⊆ {0, 1} (#35916) ... also adds a tfae for IsStarProjection in C*-algebras and that if star x * x is idempotent then so is x * star x.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Projection.lean

added theorem isIdempotentElem_iff_quasispectrum_subset

added theorem isIdempotentElem_iff_spectrum_subset

added theorem isIdempotentElem_star_mul_self_iff_isIdempotentElem_self_mul_star

Modified Mathlib/Analysis/CStarAlgebra/Projection.lean

added theorem isStarProjection_iff_quasispectrum_subset_and_isSelfAdjoint

added theorem isStarProjection_iff_quasispectrum_subset_and_isStarNormal

added theorem isStarProjection_iff_spectrum_subset_and_isSelfAdjoint

added theorem isStarProjection_iff_spectrum_subset_and_isStarNormal

Modified Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

added theorem IsIdempotentElem.finite_quasispectrum

added theorem IsIdempotentElem.finite_spectrum

modified theorem IsIdempotentElem.quasispectrum_subset