Commit 2021-10-03 06:55 7d83ff15
View on Github →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 .