Theorem CFC.negPart_eq_of_eq_PosPart_sub

Modification history

2024-11-28 17:43
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
feat: expand API for `CFC.posPart` (#19221)
Added CFC.negPart_eq_of_eq_PosPart_subView on Github →