Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-06-02 02:44
6f758e58
View on Github →
feat: uniqueness of the non-unital continuous functional calculus (
#13363
)
Estimated changes
Modified
Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean
Modified
Mathlib/Topology/ContinuousFunction/UniqueCFC.lean
added
theorem
ContinuousMapZero.continuous_toNNReal
added
theorem
ContinuousMapZero.toContinuousMapHom_toNNReal
added
theorem
ContinuousMapZero.toNNReal_add_add_neg_add_neg_eq
added
theorem
ContinuousMapZero.toNNReal_apply
added
theorem
ContinuousMapZero.toNNReal_mul_add_neg_mul_add_mul_neg_eq
added
theorem
ContinuousMapZero.toNNReal_neg_smul
added
theorem
ContinuousMapZero.toNNReal_smul
added
theorem
NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal
added
theorem
NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal
added
theorem
NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective
added
theorem
RCLike.uniqueNonUnitalContinuousFunctionalCalculus_of_compactSpace_quasispectrum