Theorem CFC.eq_negPart_iff

Modification history

2025-08-05 07:35

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Basic.lean

chore: further >6month old deprecations (#27799)

Deleted CFC.eq_negPart_iff View on Github →

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_negPart_iff View on Github →