Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-17 08:03 6a99e9e8

View on Github →

chore(analysis/calculus/deriv): add iff versions of differentiable_const_add etc (#5390) Also drop some unneeded differentiable assumptions in lemmas like deriv_const_add.

Estimated changes

modified theorem deriv_add_const
modified theorem deriv_const_add
modified theorem deriv_const_sub
modified theorem deriv_sub_const
modified theorem deriv_within.neg
modified theorem deriv_within_add_const
modified theorem deriv_within_const_add
modified theorem deriv_within_const_sub
modified theorem deriv_within_sub_const
modified theorem differentiable.const_add
modified theorem differentiable.const_sub
modified theorem differentiable.neg
modified theorem differentiable.sub_const
modified theorem differentiable_at.neg
modified theorem differentiable_at.sub_const
added theorem differentiable_neg_iff
modified theorem differentiable_on.const_add
modified theorem differentiable_on.const_sub
modified theorem differentiable_on.sub_const
modified theorem fderiv_add_const
modified theorem fderiv_const_add
modified theorem fderiv_const_sub
modified theorem fderiv_neg
modified theorem fderiv_sub_const
modified theorem fderiv_within_add_const
modified theorem fderiv_within_const_add
modified theorem fderiv_within_const_sub
modified theorem fderiv_within_neg
modified theorem fderiv_within_sub_const
modified theorem has_fderiv_at.add_const