Theorem CFC.eq_posPart_iff

Modification history

2024-10-27 18:23

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/PosPart.lean

feat: define the positive and negative parts of elements in a C⋆-algebra (#18103)

Added CFC.eq_posPart_iff View on Github →