Theorem IsSelfAdjoint.map_spectrum_real

Modification history

2026-08-20 02:52
Mathlib/Analysis/CStarAlgebra/Hom.lean
feat: `fun x ↦ x⁺` is monotone on commuting elements of a C⋆-algebra (#42785)
Modified IsSelfAdjoint.map_spectrum_realView on Github →
2024-10-24 15:52
Mathlib/Analysis/CStarAlgebra/Hom.lean
refactor: create `CStarAlgebra` classes and refactor to use them (#16953)
Modified IsSelfAdjoint.map_spectrum_realView on Github →
2024-09-11 00:28
Mathlib/Analysis/CStarAlgebra/Hom.lean
feat: star monomorphisms between C⋆-algebras are isometric (#16599)
Added IsSelfAdjoint.map_spectrum_realView on Github →