Commit 2023-05-24 22:02 8aca1d55

View on Github →

feat: port Analysis.Calculus.FDeriv.Star (#4301)

Estimated changes

Modified Mathlib.lean

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

added theorem Differentiable.star

added theorem DifferentiableAt.star

added theorem DifferentiableOn.star

added theorem DifferentiableWithinAt.star

added theorem HasFDerivAtFilter.star

added theorem HasStrictFDerivAt.star

added theorem differentiableAt_star_iff

added theorem differentiableOn_star_iff

added theorem differentiableWithinAt_star_iff

added theorem differentiable_star_iff

added theorem fderivWithin_star

added theorem fderiv_star