Theorem Unitization.isIdempotentElem_inr_iff

Modification history

2025-07-26 16:23

Mathlib/Algebra/Algebra/Unitization.lean

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

Added Unitization.isIdempotentElem_inr_iff View on Github →