Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-04 20:49
04d916cc
View on Github →
feat: port Analysis.SpecialFunctions.Sqrt (
#4529
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/SpecialFunctions/Sqrt.lean
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
DifferentiableWithinAt.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
Real.hasStrictDerivAt_sqrt
added
theorem
derivWithin_sqrt
added
theorem
deriv_sqrt
added
theorem
fderivWithin_sqrt
added
theorem
fderiv_sqrt