Commit 2023-06-04 20:49 04d916cc

View on Github →

feat: port Analysis.SpecialFunctions.Sqrt (#4529)

Estimated changes

added theorem ContDiff.sqrt
added theorem ContDiffAt.sqrt
added theorem ContDiffOn.sqrt
added theorem ContDiffWithinAt.sqrt
added theorem Differentiable.sqrt
added theorem DifferentiableAt.sqrt
added theorem DifferentiableOn.sqrt
added theorem HasDerivAt.sqrt
added theorem HasDerivWithinAt.sqrt
added theorem HasFDerivAt.sqrt
added theorem HasFDerivWithinAt.sqrt
added theorem HasStrictDerivAt.sqrt
added theorem HasStrictFDerivAt.sqrt
added theorem Real.contDiffAt_sqrt
added theorem Real.deriv_sqrt_aux
added theorem Real.hasDerivAt_sqrt
added theorem derivWithin_sqrt
added theorem deriv_sqrt
added theorem fderivWithin_sqrt
added theorem fderiv_sqrt