Commit 2023-10-16 14:39 bdfd1fa7

View on Github →

feat: lemmas about derivatives (#7683)

From the Sobolev project

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/ContDiff.lean

added theorem contDiff_single

added theorem contDiff_update

Modified Mathlib/Analysis/Calculus/Deriv/Add.lean

Created Mathlib/Analysis/Calculus/Deriv/Pi.lean

added theorem deriv_single

added theorem deriv_update

added theorem hasDerivAt_single

added theorem hasDerivAt_update

Modified Mathlib/Analysis/Calculus/FDeriv/Add.lean

added theorem hasFDerivAt_sub_const

added theorem hasStrictFDerivAt_sub_const

Created Mathlib/Analysis/Calculus/FDeriv/Pi.lean

added theorem fderiv_single

added theorem fderiv_update

added theorem hasFDerivAt_single

added theorem hasFDerivAt_update