f x * g x #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we prove formulas for
(f x * g x)' and
(f x • g x)'.
For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of
Derivative of the multiplication of a scalar function and a vector function #
Derivative of the multiplication of two functions #
Derivative of the pointwise composition/application of continuous linear maps #