Commit 2021-08-07 00:16 b3c1de6a

View on Github →

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.

Estimated changes

Modified src/analysis/calculus/fderiv.lean

added theorem differentiable_at.fderiv_restrict_scalars

added theorem differentiable_at_iff_restrict_scalars

added theorem differentiable_within_at_iff_restrict_scalars

added theorem has_fderiv_at_of_restrict_scalars

added theorem has_fderiv_within_at_of_restrict_scalars