---
tag: 0Z9JB71BS0
kind: statement
role: corollary
name: Constant multiple rule
msc: [26A24]
uses: [0M0TKFRX2A]
sources:
  - url: https://en.wikipedia.org/wiki/Linearity_of_differentiation
    locator: Constant coefficient
---

## Statement

Let $f$ be a real function on an open interval $I$, differentiable at $a \in I$, and let $c$ be a real number.
Then $c f$ is differentiable at $a$, and $(c f)'(a) = c f'(a)$.

## Remarks

It is the case $\beta = 0$ of the [[linearity of differentiation|0M0TKFRX2A]].
For example, $(5 x^2)' = 10 x$.
Mathlib states it as `deriv_const_mul`.

## Explanations

### L1 human

Stretching a graph vertically by a factor $c$ multiplies all its slopes by $c$.