Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-28 08:49
3e1d33f8
View on Github →
feat: port Analysis.Calculus.Deriv.Add (
#4435
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/Calculus/Deriv/Add.lean
added
theorem
HasDerivAt.sum
added
theorem
HasDerivAtFilter.add_const
added
theorem
HasDerivAtFilter.const_add
added
theorem
HasDerivAtFilter.const_sub
added
theorem
HasDerivAtFilter.sub
added
theorem
HasDerivAtFilter.sub_const
added
theorem
HasDerivAtFilter.sum
added
theorem
HasDerivWithinAt.sum
added
theorem
HasStrictDerivAt.const_sub
added
theorem
HasStrictDerivAt.sub
added
theorem
HasStrictDerivAt.sum
added
theorem
deriv.neg'
added
theorem
deriv.neg
added
theorem
derivWithin.neg
added
theorem
derivWithin_add
added
theorem
derivWithin_add_const
added
theorem
derivWithin_const_add
added
theorem
derivWithin_const_sub
added
theorem
derivWithin_neg
added
theorem
derivWithin_sub
added
theorem
derivWithin_sub_const
added
theorem
derivWithin_sum
added
theorem
deriv_add
added
theorem
deriv_add_const'
added
theorem
deriv_add_const
added
theorem
deriv_const_add'
added
theorem
deriv_const_add
added
theorem
deriv_const_sub
added
theorem
deriv_neg''
added
theorem
deriv_neg'
added
theorem
deriv_neg
added
theorem
deriv_sub
added
theorem
deriv_sub_const
added
theorem
deriv_sum
added
theorem
differentiableOn_neg
added
theorem
differentiable_neg
added
theorem
hasDerivAtFilter_neg
added
theorem
hasDerivAt_neg'
added
theorem
hasDerivAt_neg
added
theorem
hasDerivWithinAt_neg
added
theorem
hasStrictDerivAt_neg