Commit 2024-11-28 17:43 a315e3e5

View on Github →

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

Estimated changes

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

added theorem CFC.le_posPart

added theorem CFC.negPart_algebraMap

added theorem CFC.negPart_eq_neg

added theorem CFC.negPart_eq_of_eq_PosPart_sub

modified theorem CFC.negPart_eq_zero_iff

added theorem CFC.negPart_one

added theorem CFC.negPart_smul

added theorem CFC.negPart_smul_of_nonneg

added theorem CFC.negPart_smul_of_nonpos

added theorem CFC.negPart_zero

added theorem CFC.neg_negPart_le

added theorem CFC.posPart_algebraMap

added theorem CFC.posPart_algebraMap_nnreal

added theorem CFC.posPart_eq_of_eq_sub_negPart

added theorem CFC.posPart_eq_self

modified theorem CFC.posPart_eq_zero_iff

added theorem CFC.posPart_natCast

added theorem CFC.posPart_one

added theorem CFC.posPart_smul

added theorem CFC.posPart_smul_of_nonneg

added theorem CFC.posPart_smul_of_nonpos

added theorem CFC.posPart_zero