mem_normalizer_iff'' — Mathlib

English

An element g is in the normalizer of H if and only if for all g in G, h ∈ H ⇔ g^{-1} h g ∈ H.

Русский

Элемент g принадлежит нормализатору H тогда и только тогда, когда для всех h ∈ H сопряжение g^{-1} h g принадлежит H.

LaTeX

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

Lean4

@[to_additive]
theorem mem_normalizer_iff'' {g : G} : g ∈ H.normalizer ↔ ∀ h : G, h ∈ H ↔ g⁻¹ * h * g ∈ H := by
  rw [← inv_mem_iff (x := g), mem_normalizer_iff, inv_inv]

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