---
tag: 0F1WR9C83K
kind: definition
name: Derivative
msc: [26A24]
defines: 0V1EJCT8G6
uses: [0TXTSEMHR5]
sources:
  - url: https://en.wikipedia.org/wiki/Derivative
    locator: As a limit
---

## Definition

Let $I$ be an open interval, let $f \colon I \to \mathbb{R}$ be a function, and let $a \in I$.
A real number $L$ is the derivative of $f$ at $a$ if
$$\lim_{h \to 0} \frac{f(a + h) - f(a)}{h} = L.$$
The notation is $f'(a) = L$.

## Remarks

The quotient is the slope of the line through $(a, f(a))$ and $(a + h, f(a + h))$. The limit is a [[limit of a function|0TXTSEMHR5]] of $h$ at $0$.
The derivative is unique when it exists.
For example, the derivative of $x^2$ at $a$ is $\lim_{h \to 0} (2a + h) = 2a$.
Mathlib defines the relation "$f$ has derivative $L$ at $a$" as `HasDerivAt`.

## Explanations

### L1 human

The derivative of $f$ at $a$ is the instantaneous rate of change of $f$ at $a$.
Geometrically, it gives the steepness of the graph at the point $(a, f(a))$.