Mathlib Changelog
v4
Changelog
About
Github
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