Theorem WeakDual.CharacterSpace.homeoEval_naturality

Modification history

2024-03-28 10:26

Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean

chore: Rename `IsROrC` to `RCLike` (#10819) …

Modified WeakDual.CharacterSpace.homeoEval_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 WeakDual.CharacterSpace.homeoEval_naturality View on Github →