Sylow_p_Subgroup_is_Unique_iff_Normal
Provedgroup-theorynormal-subgroupsproofwikisylow-theorems
A group has exactly one Sylow -subgroup is normal.
Preamble
import Mathlib.GroupTheory.Sylow
Formal statement
theorem Sylow_p_Subgroup_is_Unique_iff_Normal {G : Type _} [Group G] [Fintype G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) : (∀ Q : Sylow p G, Q = P) ↔ P.toSubgroup.Normal := by sorrySource