Mathlib v3 is deprecated. Go to Mathlib v4

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, fix deriv_id'
  • Update src/analysis/calculus/deriv.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Fix compile

Estimated changes

added theorem deriv_const'
added theorem deriv_id'
modified theorem deriv_id
added theorem deriv_neg'
modified theorem deriv_neg
added theorem deriv_pow'
modified theorem deriv_pow
added theorem complex.deriv_cos'
modified theorem complex.deriv_cos
modified theorem complex.deriv_cosh
modified theorem complex.deriv_exp
modified theorem complex.deriv_sin
modified theorem complex.deriv_sinh
added theorem complex.iter_deriv_exp
added theorem real.deriv_cos'
modified theorem real.deriv_cos
modified theorem real.deriv_cosh
modified theorem real.deriv_exp
modified theorem real.deriv_sin
modified theorem real.deriv_sinh
added theorem real.iter_deriv_exp