Theorem IsSelfAdjoint.map_spectrum_real

Modification history

2024-10-24 15:52

Mathlib/Analysis/CStarAlgebra/Hom.lean

refactor: create `CStarAlgebra` classes and refactor to use them (#16953)

Modified IsSelfAdjoint.map_spectrum_real View 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_real View on Github →