Normalizer_of_Sylow_p_Subgroup

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

group-theorynormalizerproofwikisylow-theorems

Let $P$ be a Sylow $p$ -subgroup of a finite group $G$ . Let $\map {N_G} P$ be the normalizer of $P$ . Then any $p$ -subgroup of $\map {N_G} P$ is contained in $P$ . In particular, $P$ is the unique Sylow $p$ -subgroup of $\map {N_G} P$ .

Preamble

import Mathlib.GroupTheory.Sylow

Formal statement

theorem Normalizer_of_Sylow_p_Subgroup {G : Type _} [Group G] [Fintype G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) : P.toSubgroup ≤ P.toSubgroup.normalizer := by sorry

Source

https://proofwiki.org/wiki/Normalizer_of_Sylow_p-Subgroup

View graph