Commit 2023-05-22 16:36 76348246

View on Github →

feat: port Analysis.Calculus.FDeriv.RestrictScalars (#4186)

Estimated changes

Modified Mathlib.lean

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

added theorem Differentiable.restrictScalars

added theorem DifferentiableAt.fderiv_restrictScalars

added theorem DifferentiableAt.restrictScalars

added theorem DifferentiableOn.restrictScalars

added theorem DifferentiableWithinAt.restrictScalars

added theorem HasFDerivAt.restrictScalars

added theorem HasFDerivAtFilter.restrictScalars

added theorem HasFDerivWithinAt.restrictScalars

added theorem HasStrictFDerivAt.restrictScalars

added theorem differentiableAt_iff_restrictScalars

added theorem differentiableWithinAt_iff_restrictScalars

added theorem hasFDerivAt_of_restrictScalars

added theorem hasFDerivWithinAt_of_restrictScalars