English
If b = g • a and x ∈ stabilizer G a, then the image of x under stabilizerEquivStabilizer is MulAut.conj g x.
Русский
Если b = g • a и x ∈ стабилизатор G a, то образ x под stabilizerEquivStabilizer равен MulAut.conj g x.
LaTeX
$$stabilizerEquivStabilizer hg x = MulAut.conj g x$$
Lean4
/-- The natural group equivalence between the stabilizers of two elements in the same orbit. -/
def stabilizerEquivStabilizer (hg : b = g • a) : stabilizer G a ≃* stabilizer G b :=
((MulAut.conj g).subgroupMap (stabilizer G a)).trans
(MulEquiv.subgroupCongr (by rw [hg, stabilizer_smul_eq_stabilizer_map_conj g a, ← MulEquiv.toMonoidHom_eq_coe]))