fderiv

Stream: new members

[Catherine Wraback]

Hi,
I'm working on understanding derivatives in Lean and I think I understand the basics of fderiv, but I was wondering how specific I be with my proofs for derivatives. For instance, is it possible to evaluate a specific derivative of a function? Am I able to show, that the derivative of x^2 is 2x or the derivative of 2^x is ln(2)*2^x? Thanks for all the help!

[Junyan Xu]

docs#deriv_pow, docs#real.has_strict_deriv_at_const_rpow docs#deriv_exp + docs#deriv.comp + docs#deriv_mul_const?

[Bryan Gin-ge Chen]

There are also some examples of derivative computations in https://github.com/leanprover-community/mathlib/blob/master/test/differentiable.lean