One-dimensional derivatives of sums etc #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we prove formulas about derivatives of
f + g,
f - g, and
∑ i, f i x for
functions from the base field to a normed space over this field.
For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of
Derivative of the sum of two functions #
Derivative of a finite sum of functions #
Derivative of the negative of a function #
Derivative of the difference of two functions #