[Merged by Bors] - feat(geometry): first stab on Lie groups

[Nicknamen]

---

In this PR we define Lie groups and we prove smoothness of some standard maps associated with the product. We also introduce the abbreviation smooth for C^\infty.

[sgouezel]

I have shortened some proofs in the times_cont_mdiff file, I still have to look at the Lie group file per se.

[sgouezel]

This looks very nice, thanks! I mostly have minor comments.

[Nicknamen]

(Just adding random thoughts while browsing through the files):

The class Lie_group depends on two parameters, I and G, just like smooth_manifold_with_corners does. So you could extend smooth_manifold_with_corners I G instead of taking it as a class parameter.

Actually I will need to change this back as this does not work when generalizing to smooth monoids / smooth rings etc. (see the topology folder for an example). But no need to do it in this PR, I will add it to the next one

[hrmacbeth]

Sorry not to have responded to your review request, it had looked to me that you were well-supplied with more expert reviewers. It looks great!

[sgouezel]

Thanks for this (and your patience :-)
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests