Quotient_of_Sylow_P_Subgroup

Proved

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

group-theoryproofwikiquotient-groupssylow-theorems

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

Preamble

import Mathlib.GroupTheory.Sylow

Formal statement

theorem Quotient_of_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 (Subgroup.map (QuotientGroup.mk' N) P.toSubgroup) := by sorry

Source

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

View graph