Commit 2023-06-04 23:02 f712a293

View on Github →

feat: port Analysis.SpecialFunctions.ExpDeriv (#4651) This incorporates the changes from https://github.com/leanprover-community/mathlib/pull/19139 which haven't hit mathport yet due to mathport CI failing for a few days. (Hopefully it will succeed on the next run.)

Estimated changes

added theorem Complex.contDiff_exp
added theorem Complex.deriv_exp
added theorem Complex.hasDerivAt_exp
added theorem Complex.iter_deriv_exp
added theorem ContDiff.cexp
added theorem ContDiff.exp
added theorem ContDiffAt.cexp
added theorem ContDiffAt.exp
added theorem ContDiffOn.cexp
added theorem ContDiffOn.exp
added theorem ContDiffWithinAt.cexp
added theorem ContDiffWithinAt.exp
added theorem Differentiable.cexp
added theorem Differentiable.exp
added theorem DifferentiableAt.cexp
added theorem DifferentiableAt.exp
added theorem DifferentiableOn.cexp
added theorem DifferentiableOn.exp
added theorem HasDerivAt.cexp
added theorem HasDerivAt.exp
added theorem HasDerivWithinAt.cexp
added theorem HasDerivWithinAt.exp
added theorem HasFDerivAt.cexp
added theorem HasFDerivAt.exp
added theorem HasFDerivWithinAt.cexp
added theorem HasFDerivWithinAt.exp
added theorem HasStrictDerivAt.cexp
added theorem HasStrictDerivAt.exp
added theorem HasStrictFDerivAt.cexp
added theorem HasStrictFDerivAt.exp
added theorem Real.contDiff_exp
added theorem Real.deriv_exp
added theorem Real.hasDerivAt_exp
added theorem Real.iter_deriv_exp
added theorem derivWithin_cexp
added theorem derivWithin_exp
added theorem deriv_cexp
added theorem deriv_exp
added theorem fderivWithin_exp
added theorem fderiv_exp