refactor(Normed/Group/Quotient): generalise to non-abelian groups

[YaelDillies]

The goal is to apply this to free groups, whose multiplication in either argument is an isometry, but isn't commutative.

---

• depends on: [Merged by Bors] - refactor(Normed/Group/Quotient): streamline, multiplicativise #21341
• depends on: refactor: change definition of distance in normed group #35037

[github-actions]

PR summary d46874c4dd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Subgroup.continuousConstSMul
+ instNormedGroup
+ instSeminormedGroup
+ instance (priority := 100) NormedGroup.to_isIsometricSMul_left : IsIsometricSMul E E
+ instance (priority := 100) SeminormedGroup.toIsTopologicalGroup : IsTopologicalGroup E
+ instance (priority := 100) SeminormedGroup.to_isUniformGroup : IsUniformGroup E
+ instance (priority := 100) SeminormedGroup.to_lipschitzMul : LipschitzMul E
+ isPretransitive_mulOpposite_quotient
- NormedGroup.to_isIsometricSMul_left

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - refactor(Normed/Group/Quotient): streamline, multiplicativise #21341
• refactor: change definition of distance in normed group #35037
  By Dependent Issues (🤖). Happy coding!

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[sgouezel]

I don't understand the comment in the PR description. In the free group with the word distance wrt the standard set of generators, left-multiplication is indeed an isometry, but right-multiplication is not. For instance, d (a, b) = 2 and d (ab, b^2) = 4.

[sgouezel]

In fact, looking at our definition of SeminormedGroup, the distance is given by dist x y = ‖x / y‖. This looks bad: for this distance, left-multiplication is not an isometry, and x is not close to xs if s is small. Am I missing something?

[YaelDillies]

Yes, I agree. Will you refactor SeminormedGroup to make right multiplication an isometry? I believe this is what's needed to make the current PR non-stupid.

[sgouezel]

I am making left-multiplication an isometry in #35037. It builds, but I'll need to split it a little bit to make it reviewable.