English
The normalizer of a Sylow p-subgroup is stable under taking normalizers; i.e., N_G(P) has itself as its normalizer.
Русский
Нормализатор нормализатора подгруппы Sylow остаётся тем же самым нормализатором.
LaTeX
$$$\forall {G:\ TYPE u} [Group\ G] {p: \mathbb{N}} [Fact p.Prime] [Finite (Sylow p G)] (P: Sylow p G), P.normalizer.normalizer = P.normalizer$$
Lean4
@[simp]
theorem normalizer_normalizer {p : ℕ} [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) :
P.normalizer.normalizer = P.normalizer :=
by
have := normal_of_normalizer_normal (P.subtype (le_normalizer.trans le_normalizer))
rw [coe_subtype, normal_subgroupOf_iff_le_normalizer (le_normalizer.trans le_normalizer), ←
subgroupOf_normalizer_eq (le_normalizer.trans le_normalizer)] at this
exact le_antisymm (this normal_in_normalizer) le_normalizer
