feat(analysis/normed/group/basic): Multiplicative, noncommutative normed groups

[YaelDillies]

Define

• seminormed_group
• seminormed_add_group
• seminormed_comm_group
• normed_group
• normed_add_group
• normed_comm_group

Additivize all lemmas in analysis.normed.group.basic. To disambiguate names, I add one or two ' to the multiplicative version where needed.

---

• [x] depends on: #15702
• [x] depends on: #15704
• [x] depends on: #15898

Do we want to have different notation for additive and multiplicative norms? This would fix the lemma homonymy problem, but I can't think of any type that's normed both additively and multiplicatively, except punit, and the norm symbol is quite unambiguous (do we really want ∥x∥ₘ and ∥x∥ₘ₊?).

I declare making the norm left-invariant (it is currently right-invariant) future work because:

• It's not clear whether we actually want to do that.
• The diff is already huge.
• This would involve fixing other files.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#15702~~
• ~~leanprover-community/mathlib#15704~~
• ~~leanprover-community/mathlib#15898~~ By Dependent Issues (🤖). Happy coding!

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

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