Commit 2026-02-24 15:42 22a74288

refactor: change definition of distance in normed group (#35037) The current definition of the distance in a normed group is dist x y = ||x / y||. With this definition, the distance is right-invariant. This does not correspond to the convention in geometric group theory where the distance is given by ||x^{-1} * y|| to make sure it is left-invariant -- this corresponds to the fact that, in a Cayley graph, we put an edge between x and xs and declare these to be at distance one. We refactor the definition to make sure it follows the standard convention. A pain point is that, in additive commutative groups, which is arguably the most important case, it becomes ||-x + y|| instead of ||x - y|| (which is propositionally the same, but not definitionally). To minimize the hassle, we keep all the lemmas that use ||x - y||, with their current names, and add new versions in terms of ||-x + y|| when useful.