Derivatives of functions taking values in product types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we prove lemmas about derivatives of functions
f : 𝕜 → E × F and of functions
f : 𝕜 → (Π i, E i).
For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of
Derivative of the cartesian product of two functions #
Derivatives of functions
f : 𝕜 → Π i, E i #