Isometry group of pseudo_emetric space splits

Stream: Is there code for X?

[Rémi Bottinelli]

If I'm not mistaken, the isometry group of a pseudo_emetric space splits as a semidirect product, with first part taking care of permuting the pseudo_metric components, and the other fixing them. Does such a decomposition exist ? I haven't found it in topology/metric_space/isometry.lean.