equivalence of stabilizers

Stream: PR reviews

[Antoine Chambert-Loir]

I have two concurrent PR giving, for a group action, the mul-equivalences between stabilizers associated with group elements, and their properties.

• #24107 is the one I need for later work, it defines stabilizer G a ≃* stabilizer G b associated with an equality b = g • a.

• #24039 defines stabilizer G a ≃* stabilizer G (g • a).

One may discuss, moreover, the natural direction of these equivalences.

[Antoine Chambert-Loir]

The interest of the first version is that the transitivity formula naturally fits in docs#CompTriple.
It is used in #23962.