Theorem map_isSelfAdjoint

Modification history

2026-06-23 15:06

Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean

feat: introduce `SelfAdjointDecompose` class (#40530)

Deleted map_isSelfAdjoint View on Github →

2025-03-30 03:51

Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean

feat(CStarAlgebra): define positive maps and show their continuity (#23210) …

Added map_isSelfAdjoint View on Github →