mathlib
c0693ca0 - chore(analysis/calculus/*): add `filter.eventually_eq.deriv` etc. (#9131)

Commit
4 years ago
chore(analysis/calculus/*): add `filter.eventually_eq.deriv` etc. (#9131) * add `filter.eventually_eq.deriv` and `filter.eventually_eq.fderiv`; * add `times_cont_diff_within_at.eventually` and `times_cont_diff_at.eventually`.
Author
Parents
Loading