characteristic_centralizer — Mathlib

English

If H is a characteristic subgroup of G, then the centralizer of H is a characteristic subgroup of G.

Русский

Если H характеристическая подгруппа G, то центроцентрализатор H характеристическая в G.

LaTeX

$$H \text{ characteristic in } G \Rightarrow centralizer(H) \text{ characteristic in } G$$

Lean4

@[to_additive]
instance characteristic_centralizer [hH : H.Characteristic] : (centralizer (H : Set G)).Characteristic :=
  by
  refine Subgroup.characteristic_iff_comap_le.mpr fun ϕ g hg h hh => ϕ.injective ?_
  rw [map_mul, map_mul]
  exact hg (ϕ h) (Subgroup.characteristic_iff_le_comap.mp hH ϕ hh)

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