Fifth_Sylow_Theorem
Provedgroup-theoryindexproofwikisylow-theorems
The number of Sylow -subgroups of a finite group is a divisor of their common index.
Preamble
import Mathlib.GroupTheory.Sylow
Formal statement
theorem Fifth_Sylow_Theorem {G : Type _} [Group G] [Fintype G] {p : ℕ} [Fact (Nat.Prime p)] : Fintype.card (Sylow p G) ∣ Fintype.card G := by sorrySource