How to calculate derivatives

Stream: maths

[Moritz Doll]

Say you have a function λ x, f x * g x / c and the derivatives of f and g and you want to prove that it has derivative λ x, h x + h' x, what is the most efficient way to do that? My idea would be to first show has_deriv_at (λ x, f x * g x / c) (..) x0, where (..) is the expression coming from using has_deriv_at.div_const and has_deriv_at.mul and then use uniqueness of the derivative to convert the rest to (annoying) algebraic calculations. This sounds extremely tedious and not elegant to me, so is there a better way?

[Heather Macbeth]

Maybe something like

convert (hf.mul hg).div_const,
[...algebraic calculations...]

[Heather Macbeth]

I don't think that uses the uniqueness of the derivative?

[Moritz Doll]

thanks, you are of course right, that this does not need the uniqueness

[Violeta Hernández]

Yeah, it's quite odd that the Taylor polynomial isn't a polynomial

[Eric Wieser]

Wrong thread?