mathlib
beb6831f - feat(analysis/calculus/times_cont_diff): add `restrict_scalars` (#4899)

Commit
5 years ago
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`.
Author
Parents
Loading