Commit 2023-07-16 11:35 b15b2bff

View on Github →

chore: forward-port leanprover-community/mathlib#19127 (#5889)

Estimated changes

added theorem Differentiable.inv'
added theorem Differentiable.inverse
added theorem DifferentiableAt.inv'
added theorem DifferentiableOn.inv'
added theorem differentiableAt_inv'
modified theorem differentiableAt_inverse
added theorem differentiableOn_inv'
added theorem fderivWithin_inv'
added theorem fderiv_inv'
added theorem hasFDerivAt_inv'