mathlib3
8f5cf785 - chore(analysis/calculus/fderiv): squeeze simps (#17344)

Commit
3 years ago
chore(analysis/calculus/fderiv): squeeze simps (#17344) Profiling: * differentiable_at.fderiv_within: 9.56ms -> 5.49ms * differentiable_on_univ: 40.6ms -> 6.23ms * has_fderiv_at_filter.tendsto_nhds: 962ms -> 452ms * has_strict_fderiv_at.add: 21.5s -> 4.79s * has_fderiv_at_filter.add: 11.3s -> 2.84s
Author
Parents
Loading