Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-02 19:10 840bd1f5

View on Github →

feat(analysis/calculus/deriv): add aliases for const op f and f op const (#1843)

  • feat(analysis/calculus/deriv): add aliases for const op f and f op const Often this leads to simpler answers.
  • Docs
  • Fix compile of mean_value.lean
  • Drop comments, use open_locale classical

Estimated changes

added theorem deriv_add_const
added theorem deriv_const_add
added theorem deriv_const_mul
added theorem deriv_const_smul
added theorem deriv_const_sub
added theorem deriv_mul_const
deleted theorem deriv_smul'
added theorem deriv_smul
added theorem deriv_smul_const
added theorem deriv_sub_const
added theorem deriv_within_add_const
added theorem deriv_within_const_add
added theorem deriv_within_const_mul
added theorem deriv_within_const_sub
added theorem deriv_within_mul_const
deleted theorem deriv_within_smul'
added theorem deriv_within_smul
added theorem deriv_within_sub_const
added theorem has_deriv_at.add_const
added theorem has_deriv_at.const_add
added theorem has_deriv_at.const_mul
added theorem has_deriv_at.const_sub
added theorem has_deriv_at.mul_const
deleted theorem has_deriv_at.smul'
added theorem has_deriv_at.smul
added theorem has_deriv_at.sub_const
deleted theorem has_deriv_within_at.smul'
deleted theorem differentiable.smul'
modified theorem differentiable.smul
deleted theorem differentiable_at.smul'
modified theorem differentiable_at.smul
deleted theorem differentiable_on.smul'
modified theorem differentiable_on.smul
added theorem fderiv_add_const
added theorem fderiv_const_add
added theorem fderiv_const_mul
added theorem fderiv_const_smul
added theorem fderiv_const_sub
added theorem fderiv_mul_const
deleted theorem fderiv_smul'
modified theorem fderiv_smul
added theorem fderiv_smul_const
added theorem fderiv_sub_const
deleted theorem fderiv_within_smul'
deleted theorem has_fderiv_at.smul'
modified theorem has_fderiv_at.smul
deleted theorem has_fderiv_at_filter.smul
modified theorem has_fderiv_within_at.smul
added theorem has_deriv_at.cexp
added theorem has_deriv_at.rexp