Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-13 12:44 6625f663

View on Github →

feat(analysis/calculus/deriv): one-dimensional derivatives (#1670)

  • feat(analysis/calculus/deriv): one-dimensional derivatives
  • Typos.
  • Define deriv f x as fderiv 𝕜 f x 1
  • Proof style.
  • Fix failing proofs.

Estimated changes

added theorem deriv.comp
added def deriv
added theorem deriv_add
added theorem deriv_const
added theorem deriv_fderiv
added theorem deriv_id
added theorem deriv_mul
added theorem deriv_neg
added theorem deriv_sub
added theorem deriv_within.comp
added def deriv_within
added theorem deriv_within_add
added theorem deriv_within_congr
added theorem deriv_within_const
added theorem deriv_within_id
added theorem deriv_within_inter
added theorem deriv_within_mul
added theorem deriv_within_neg
added theorem deriv_within_sub
added theorem deriv_within_subset
added theorem deriv_within_univ
added theorem fderiv_deriv
added theorem has_deriv_at.add
added theorem has_deriv_at.comp
added theorem has_deriv_at.deriv
added theorem has_deriv_at.mul
added theorem has_deriv_at.neg
added theorem has_deriv_at.prod
added theorem has_deriv_at.sub
added def has_deriv_at
added theorem has_deriv_at_const
added theorem has_deriv_at_filter_id
added theorem has_deriv_at_id
added theorem has_deriv_at_unique
added theorem has_deriv_within_at_id
added theorem is_linear_map.deriv
added theorem algebra.id.map_eq_self
added theorem algebra.id.smul_eq_mul