How do I take the derivative of a rational function？

Stream: new members

[Junqi Liu]

For rational function like $\frac{1}{ax}$, how to take $x$-derivative of it?

[Luigi Massacci]

Have you looked at docs#iteratedFDeriv ?

[Luigi Massacci]

Ah sorry I substituted "nth-derivative" in place of "x-derivative" in my brain, you probably want just docs#deriv then

[Vincent Beffara]

Look at docs#HasDerivAt.inv and docs#hasDerivAt_mul_const for instance

[Junqi Liu]

oh! I'll have a try! But I don't understand how to deal with the condition : HasDerivAt

[Luigi Massacci]

You are probably better off posting a #mwe

[Vincent Beffara]

What do you want to do exactly? If you want to prove that the derivative of 1/ax at x (not zero) exists and is is what it should be, then this will be the statement of your lemma (stated in terms of HasDerivAt) and the proof will involve lemmas like the ones I mentioned or very similar ones. If you want Lean to compute the derivative for you, AFAIK it won't and you will end up being very disappointed ...