normalizerMonoidHom_ker — Mathlib

English

The kernel of the normalizer action equals the centralizer of H inside the normalizer.

Русский

Ядро действия нормализатора равно центральизатору H внутри нормализатора.

LaTeX

$$$\ker(H.normalizerMonoidHom) = (\mathrm{centralizer} H).subgroupOf (H.normalizer)$$$

Lean4

theorem normalizerMonoidHom_ker : H.normalizerMonoidHom.ker = (Subgroup.centralizer H).subgroupOf H.normalizer := by
  simp [Subgroup.ext_iff, DFunLike.ext_iff, Subtype.ext_iff, mem_subgroupOf, mem_centralizer_iff, eq_mul_inv_iff_mul_eq,
    eq_comm]

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