mem_normalizer_iff — Mathlib

English

An element g lies in the normalizer of H if and only if conjugating every element of H by g yields an element of H.

Русский

Элемент g принадлежит нормализатору H тогда и только тогда, когда сопряжение каждого элемента H с g возвращает элемент H.

LaTeX

$$$g \\in N_G(H) \\iff \\forall n \\in H, g n g^{-1} \\in H$$$

Lean4

@[to_additive]
theorem mem_normalizer_iff {g : G} : g ∈ H.normalizer ↔ ∀ h, h ∈ H ↔ g * h * g⁻¹ ∈ H :=
  Iff.rfl

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