Commit 2024-01-12 03:12 fa19a556

View on Github →

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

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean

modified theorem WeakDual.CharacterSpace.compContinuousMap_comp

added theorem WeakDual.CharacterSpace.homeoEval_naturality

added theorem gelfandStarTransform_naturality