English
The set normalizer of S is the subgroup of G consisting of elements g such that g S g^{-1} = S.
Русский
Нормализатор множества S — это подгруппа G, состоящая из элементов g, для которых g S g^{-1} = S.
LaTeX
$$$N_G(S) = \\{ g \\in G \\mid g S g^{-1} = S \\}$$$
Lean4
/-- The `setNormalizer` of `S` is the subgroup of `G` whose elements satisfy `g*S*g⁻¹=S` -/
@[to_additive /-- The `setNormalizer` of `S` is the subgroup of `G` whose elements satisfy
`g+S-g=S`. -/
]
def setNormalizer (S : Set G) : Subgroup G
where
carrier := {g : G | ∀ n, n ∈ S ↔ g * n * g⁻¹ ∈ S}
one_mem' := by simp
mul_mem' {a b} (ha : ∀ n, n ∈ S ↔ a * n * a⁻¹ ∈ S) (hb : ∀ n, n ∈ S ↔ b * n * b⁻¹ ∈ S)
n := by
rw [hb, ha]
simp only [mul_assoc, mul_inv_rev]
inv_mem' {a} (ha : ∀ n, n ∈ S ↔ a * n * a⁻¹ ∈ S)
n := by
rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]
