English
The normalizer N_G(H) is the largest subgroup of G inside which H is normal.
Русский
Нормализатор N_G(H) — наибольшая подгруппа G, внутри которой H нормальна.
LaTeX
$$$N_G(H) = \\{ g \\in G \\mid g H g^{-1} = H \\}$$$
Lean4
/-- The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal. -/
@[to_additive /-- The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal. -/
]
def normalizer : Subgroup G where
carrier := {g : G | ∀ n, n ∈ H ↔ g * n * g⁻¹ ∈ H}
one_mem' := by simp
mul_mem' {a b} (ha : ∀ n, n ∈ H ↔ a * n * a⁻¹ ∈ H) (hb : ∀ n, n ∈ H ↔ b * n * b⁻¹ ∈ H)
n := by
rw [hb, ha]
simp only [mul_assoc, mul_inv_rev]
inv_mem' {a} (ha : ∀ n, n ∈ H ↔ a * n * a⁻¹ ∈ H)
n := by
rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]
-- variant for sets.
-- TODO should this replace `normalizer`?
