Theorem CFC.negPart_mul_posPart

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