mathlib3

b3c1de6a - feat(analysis/complex/basic): add several trivial lemmas for differentiable functions. (#8418)

feat(analysis/complex/basic): add several trivial lemmas for differentiable functions. (#8418) This file relates the differentiability of a function to the linearity of its `fderiv`. Co-authored-by: justadzr <66561890+justadzr@users.noreply.github.com>