fixingSubgroup_smul_eq_fixingSubgroup_map_conj

English

The fixingSubgroup of a translate is isomorphic to the fixingSubgroup of the original via conjugation.

Русский

Фиксирующая подгруппа переноса изоморфна фиксирующей подгруппе исходного множества через конъюгацию.

LaTeX

$$$fixingSubgroup M (g\cdot s) \cong fixingSubgroup M s$ via conjugation$$

Lean4

/-- The `fixingSubgroup` of `g • s` is the conjugate of the `fixingSubgroup` of `s` by `g`. -/
@[to_additive /-- The `fixingAddSubgroup` of `g +ᵥ s` is the conjugate
    of the `fixingAddSubgroup` of `s` by `g`. -/
    ]
theorem fixingSubgroup_smul_eq_fixingSubgroup_map_conj :
    fixingSubgroup M (g • s) = (fixingSubgroup M s).map (MulAut.conj g).toMonoidHom :=
  (fixingSubgroup_map_conj_eq rfl).symm

Похожие утверждения