Second_Sylow_Theorem

Proved

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

group-theoryp-subgroupsproofwikisylow-theorems

Let $P$ be a Sylow $p$ -subgroup of the finite group $G$ . Let $Q$ be any $p$ -subgroup of $G$ . Then $Q$ is a subset of a conjugate of $P$ .

Preamble

import Mathlib.GroupTheory.Sylow

Formal statement

theorem Second_Sylow_Theorem {G : Type _} [Group G] [Fintype G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) (Q : Subgroup G) [Fintype Q] (hQ : IsPGroup p Q) : ∃ g : G, Q ≤ Subgroup.map (MulAut.conj g).toMonoidHom P.toSubgroup := by sorry

Source

https://proofwiki.org/wiki/Second_Sylow_Theorem

View graph