Theorem CFC.posPart_mul_negPart

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