Theorem CFC.real_exp_eq_normedSpace_exp

Modification history

2024-09-02 17:15
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
feat(ContinuousFunctionalCalculus): add lemmas for automation and simp/aesop tags (#16050) …
Modified CFC.real_exp_eq_normedSpace_expView on Github →
2024-07-17 03:09
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
feat(ContinuousFunctionalCalculus): Define the real log based on the CFC (#14448) …
Added CFC.real_exp_eq_normedSpace_expView on Github →