Commit 2022-05-07 09:57 b2aa27e3

View on Github →

feat(analysis/calculus/deriv): generalize some lemmas (#13575) The types of scalar and codomain can be different now. For example, these lemmas can be used for f : ℝ → ℂ f' : ℝ →L[ℝ] ℂ now.

Estimated changes

Modified src/analysis/calculus/deriv.lean

modified theorem has_deriv_at.comp_has_fderiv_at

modified theorem has_deriv_at.comp_has_fderiv_within_at

modified theorem has_deriv_at_filter.comp_has_fderiv_at_filter

modified theorem has_deriv_within_at.comp_has_fderiv_within_at

modified theorem has_strict_deriv_at.comp_has_strict_fderiv_at