Fourth_Sylow_Theorem

Proved

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

congruencegroup-theoryproofwikisylow-theorems

The number of Sylow $p$ -subgroups of a finite group is congruent to $1 \pmod p$ .

Preamble

import Mathlib.GroupTheory.Sylow

Formal statement

theorem Fourth_Sylow_Theorem {G : Type _} [Group G] [Fintype G] {p : ℕ} [Fact (Nat.Prime p)] : Fintype.card (Sylow p G) % p = 1 % p := by sorry

Source