Theorem CFC.negPart_eq_zero_iff

Modification history

2024-11-28 17:43

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean

feat: expand API for `CFC.posPart` (#19221)

Modified CFC.negPart_eq_zero_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.negPart_eq_zero_iff View on Github →