normal_centralizer — Mathlib

English

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

Русский

Если H — нормальная подгруппа G, тогда центроцентрализатор H нормальная подпгруппа G.

LaTeX

$$(centralizer(H) : Subgroup G) \trianglelefteq G$$

Lean4

@[to_additive]
instance normal_centralizer [H.Normal] : (centralizer H : Subgroup G).Normal where
  conj_mem g hg i h
    hh := by
    simpa [-mul_left_inj, -mul_right_inj, mul_assoc] using congr(i * $(hg _ <| ‹H.Normal›.conj_mem _ hh i⁻¹) * i⁻¹)

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