Commit 2026-08-20 02:52 d77ef074

View on Github →

feat: fun x ↦ x⁺ is monotone on commuting elements of a C⋆-algebra (#42785)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

added theorem Function.Injective.isSelfAdjoint_apply_iff

added theorem IsSelfAdjoint.of_map

added theorem Subtype.isSelfAdjoint_mk_iff

Created Mathlib/Analysis/CStarAlgebra/Commutative/PosPart.lean

added theorem ContinuousMap.realToRCLike_negPart

added theorem ContinuousMap.realToRCLike_posPart

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean

added theorem cfc_nnreal_mem

added theorem cfcₙ_nnreal_mem

Modified Mathlib/Analysis/CStarAlgebra/Fuglede.lean

Modified Mathlib/Analysis/CStarAlgebra/Hom.lean

added theorem IsSelfAdjoint.map_quasispectrum_real

modified theorem IsSelfAdjoint.map_spectrum_real

added def NonUnitalStarAlgHom.toOrderEmbedding