Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-09 07:40 acd769af

View on Github →

feat(analysis/calculus/deriv): derivative of division and polynomials (#1769)

  • feat(data/set/intervals): more properties of intervals
  • fix docstrings
  • blank space
  • iff versions
  • fix docstring
  • more details in docstrings
  • initial commit
  • div_deriv
  • more derivatives
  • cleanup
  • better docstring
  • fix
  • better
  • minor fix
  • simp attributes
  • Update src/analysis/calculus/deriv.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
  • Update src/analysis/calculus/deriv.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
  • nolint
  • pow derivative
  • Update src/topology/continuous_on.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • comp_add and friends
  • remove useless variable

Estimated changes

added theorem deriv_div
added theorem deriv_inv
added theorem deriv_pow
added theorem deriv_within_div
added theorem deriv_within_inv
added theorem deriv_within_pow
added theorem differentiable.div
added theorem differentiable_at.div
added theorem differentiable_at_inv
added theorem differentiable_at_pow
added theorem differentiable_on.div
added theorem differentiable_on_inv
added theorem differentiable_on_pow
added theorem differentiable_pow
added theorem fderiv_inv
added theorem fderiv_within_inv
added theorem has_deriv_at.div
added theorem has_deriv_at_inv
added theorem has_deriv_at_inv_one
added theorem has_deriv_at_pow
added theorem has_fderiv_at_inv
added theorem filter.tendsto.div
added theorem filter.tendsto.inv'