Theorem ContinuousMap.realToRCLike_posPart

Modification history

2026-08-20 02:52
Mathlib/Analysis/CStarAlgebra/Commutative/PosPart.lean
feat: `fun x ↦ x⁺` is monotone on commuting elements of a C⋆-algebra (#42785)
Added ContinuousMap.realToRCLike_posPartView on Github →