Commit 2019-12-27 11:08 89854fa3
View on Github →refactor(analysis/calculus/deriv): Use equality of functions (#1818)
- refactor(analysis/calculus/deriv): Use equality of functions
This way we can rewrite, e.g., in
deriv (deriv sin)
. - Restore some old lemmas
- Restore old
deriv_cos
, fixderiv_id'
- Update src/analysis/calculus/deriv.lean Co-Authored-By: Johan Commelin johan@commelin.net
- Fix compile