Commit 2025-03-31 08:28 363660f4

View on Github →

feat(Analysis/Calculus): lemmas about derivatives of constant functions (#23310) See discussion on Zulip

Estimated changes

added theorem HasStrictDerivAt_ofNat
added theorem derivWithin_intCast
added theorem derivWithin_natCast
added theorem derivWithin_ofNat
added theorem derivWithin_one
added theorem deriv_intCast
added theorem deriv_natCast
added theorem deriv_ofNat
added theorem deriv_one
added theorem deriv_zero
added theorem hasDerivAtFilter_ofNat
added theorem hasDerivAtFilter_one
added theorem hasDerivAtFilter_zero
added theorem hasDerivAt_intCast
added theorem hasDerivAt_natCast
added theorem hasDerivAt_ofNat
added theorem hasDerivAt_one
added theorem hasDerivAt_zero
added theorem hasDerivWithinAt_ofNat
added theorem hasDerivWithinAt_one
added theorem hasDerivWithinAt_zero
added theorem hasStrictDerivAt_one
added theorem hasStrictDerivAt_zero
added theorem differentiableAt_ofNat
added theorem differentiableAt_one
added theorem differentiableAt_zero
added theorem differentiableOn_ofNat
added theorem differentiableOn_one
added theorem differentiableOn_zero
added theorem differentiable_intCast
added theorem differentiable_natCast
added theorem differentiable_ofNat
added theorem differentiable_one
added theorem differentiable_zero
added theorem fderivWithin_intCast
added theorem fderivWithin_natCast
added theorem fderivWithin_ofNat
added theorem fderivWithin_one
added theorem fderivWithin_zero
added theorem fderiv_intCast
added theorem fderiv_natCast
added theorem fderiv_ofNat
added theorem fderiv_one
added theorem fderiv_zero
added theorem hasFDerivAtFilter_one
added theorem hasFDerivAtFilter_zero
added theorem hasFDerivAt_intCast
added theorem hasFDerivAt_natCast
added theorem hasFDerivAt_ofNat
added theorem hasFDerivAt_one
added theorem hasFDerivAt_zero
added theorem hasFDerivWithinAt_one
added theorem hasFDerivWithinAt_zero
added theorem hasStrictFDerivAt_one
added theorem hasStrictFDerivAt_zero