Commit 2025-07-26 16:23 6fa21dbb

View on Github →

feat(Analysis/CStarAlgebra/...): an idempotent element in a C*-algebra is self-adjoint iff it is normal (#27475)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Unitization.lean

added theorem Unitization.isIdempotentElem_inr_iff

Created Mathlib/Analysis/CStarAlgebra/Projection.lean

added theorem IsIdempotentElem.isSelfAdjoint_iff_isStarNormal

added theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal

Modified Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

added theorem IsIdempotentElem.quasispectrum_subset

added theorem IsIdempotentElem.spectrum_subset