[Merged by Bors] - feat(analysis/calculus/times_cont_diff): continuous affine maps are smooth

[ocfnash]

Formalized as part of the Sphere Eversion project.

---

I considered placing this next to the lemma continuous_linear_map.times_cont_diff but I chose not to because:

• I need to use times_cont_diff.add which only appears about 500 lines lower down in the same file (analysis/calculus/times_cont_diff.lean)
• The file analysis/calculus/times_cont_diff.lean is already 3000 lines long
• It seems a shame to make all of calculus depend upon the theory of affine spaces just for this one lemma

[sgouezel]

Could you put it into its own file? Here you are importing all of calculus into continuous_affine_map, which is not much better.

[sgouezel]

Move it to calculus and I'm gonna be happy :-)
bors d+

[bors]

✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ocfnash]

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests