Theorem gelfandStarTransform_naturality

Modification history

2024-10-24 15:52

Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean

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

Modified gelfandStarTransform_naturality View on Github →

2024-01-12 03:12

Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean

feat: naturality of the `gelfandStarTransform` and `WeakDual.CharacterSpace.homeoEval` (#9638)

Added gelfandStarTransform_naturality View on Github →