ThmDex – An index of mathematical definitions, results, and conjectures.
F12573
Formulation 0
Let $f, g : \mathbb{R} \to \mathbb{R}$ each be a D5614: Differentiable real function such that
(i) \begin{equation} h : \mathbb{R} \to \mathbb{R}, \quad h(x) = f(x) g(x) \end{equation}
Then
(1) $h$ is a D5614: Differentiable real function
(2) \begin{equation} h'(x) = f'(x) g(x) + f(x) g'(x) \end{equation}