Commit 2020-11-04 08:09 beb6831f

View on Github →

feat(analysis/calculus/times_cont_diff): add restrict_scalars (#4899) Add restrict_scalars lemmas to has_ftaylor_series_up_to_on, times_cont_diff_within_at, times_cont_diff_on, times_cont_diff_at, and times_cont_diff.

Estimated changes

Modified src/analysis/calculus/times_cont_diff.lean

added def formal_multilinear_series.restrict_scalars

added theorem has_ftaylor_series_up_to_on.restrict_scalars

added theorem times_cont_diff.restrict_scalars

added theorem times_cont_diff_at.restrict_scalars

added theorem times_cont_diff_on.restrict_scalars

added theorem times_cont_diff_within_at.restrict_scalars