Intersection_of_Normal_Subgroup_with_Sylow_P_Subgroup

Proved

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

group-theorynormal-subgroupsproofwikisylow-theorems

Let $P$ be a Sylow $p$ -subgroup of a finite group $G$ . Let $N$ be a normal subgroup of $G$ . Then $P \cap N$ is a Sylow $p$ -subgroup of $N$ .

Preamble

import Mathlib.GroupTheory.Sylow

Formal statement

theorem Intersection_of_Normal_Subgroup_with_Sylow_P_Subgroup {G : Type _} [Group G] [Fintype G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) (N : Subgroup G) [N.Normal] : IsPGroup p (N.subgroupOf P.toSubgroup) := by sorry

Source

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

View graph