Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-09 13:20 97e44687

View on Github →

feat(analysis/calculus/deriv): generalize some lemmas (#10639) Generalize lemmas about the chain rule to work with different fields.

Estimated changes

Modified src/analysis/calculus/deriv.lean

modified theorem has_deriv_within_at.comp

modified theorem has_deriv_within_at.scomp

Modified src/analysis/calculus/fderiv.lean

modified theorem has_fderiv_at_filter.comp

added theorem has_fderiv_at_filter.restrict_scalars

Modified src/measure_theory/integral/interval_integral.lean