Linearity of differentiation

Statement

Let $f$ and $g$ be real functions on an open interval $I$, both differentiable at $a \in I$. Let $\alpha$ and $\beta$ be real numbers. Then $\alpha f + \beta g$ is differentiable at $a$, and $$(\alpha f + \beta g)'(a) = \alpha f'(a) + \beta g'(a).$$

Remarks

The difference quotient of $\alpha f + \beta g$ is $\alpha$ times that of $f$ plus $\beta$ times that of $g$. The limit laws give the result. The case $\alpha = \beta = 1$ is the sum rule $(f + g)' = f' + g'$. The case $\beta = 0$ is the constant multiple rule. Mathlib states the sum rule as deriv_add.

Explanations

L1 human

Differentiation respects sums and constant factors. So we can differentiate a sum term by term.