Theorem NormedSpace.exp_continuousMap_eq

Modification history

2024-07-17 03:09
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
feat(ContinuousFunctionalCalculus): Define the real log based on the CFC (#14448) …
Added NormedSpace.exp_continuousMap_eqView on Github →