[[!redirects derivative]] #Contents# * table of contents {:toc} ## Definition ## Given a [[calculus field]] $F$ and a subtype $S \subseteq F$, the __Newton–Leibniz operator__ $\tilde{D}: D^1(S, F) \to (S \to F)$ is a function from the type of [[differentiable function]]s $D^1(S, F)$ to the type of functions $S \to F$ that is pointwise defined as $$\tilde{D}(f) \coloneqq \lim_{(x, y) \to (x, x)} \frac{f(x) - f(y)}{x - y}$$ for a [[differentiable function]] $f:D^1(S, F)$. For any differentiable function $f:D^1(S, F)$, the function $\tilde{D}(f)$ is called the __derivative__ of $f$. ## Properties ## These all follow from the algebraic limit theorems, which are axioms used to define a [[calculus field]]. ### Linearity ### ### Leibniz rule ### ### Power rule ### ### Quotient rule ### ## See also ## * [[differentiable function]] * [[iterated differentiable function]] * [[smooth function]]