Commit 2024-05-19 22:59 38aa2fc7
View on Github →chore(Analysis/SpecialFunctions/Exp): deal with TODO (#12781)
This deals with the TODO in Mathlib.Analysis.SpecialFuncitons.Exp:L146 by renaming Continuous{WithinAt|At|On|}.exp to ...rexp.
Rationale: These are not in the Real namespace, and there are at least three different exponentials in Mathlib (Real.exp, Complex.exp and NormedSpace.exp), so it is better to make clear which one is used in these declarations.