Commit 2020-07-27 01:32 d06f62d5

feat(analysis/calculus/times_cont_diff): more thorough times_cont_diff interface (#3551) Add missing lemmas on smooth functions between vector spaces, that were necessary to solve the manifold exercises in Lftcm2020. Changes the {x : E} argument from implicit to explicit in lemma times_cont_diff_within_at.comp and lemma times_cont_diff_within_at.comp'.