Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-01 16:14 8a89b063

View on Github →

refactor(analysis/calculus/mean_value): prove the mean value theorem using 1D derivative (#1740)

refactor(analysis/calculus/mean_value): prove the mean value theorem using 1D derivative
docstring
use iff.rfl
fix build
fix docstring

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem deriv_smul'

added theorem deriv_within_smul'

added theorem fderiv.comp_deriv

added theorem fderiv_within.comp_deriv_within

added theorem has_deriv_at.smul'

added theorem has_deriv_within_at.smul'

added theorem has_fderiv_at.comp_has_deriv_at

added theorem has_fderiv_at.comp_has_deriv_within_at

added theorem has_fderiv_within_at.comp_has_deriv_within_at

Modified src/analysis/calculus/fderiv.lean

deleted theorem differentiable.fderiv_within

added theorem differentiable_at.fderiv_within

Modified src/analysis/calculus/mean_value.lean