mathlib

7d83ff15 - feat(analysis/special_functions/exp_log): prove continuity of exp without derivatives (#9501)

feat(analysis/special_functions/exp_log): prove continuity of exp without derivatives (#9501) This is a first step towards making the definition of log and rpow independent of derivatives. The final goal is to avoid importing all of calculus in measure_theory/function/lp_space.lean .