TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Sylow III*: $n_{p} (G) = [G : N_{G} (P)]$

Statement

If $P$ is a Sylow $p$ -subgroup of a finite group $G$ , then $n_{p} (G) = [G : N_{G} (P)] .$ See Sylow II: in a finite group every $p$ -subgroup lies in a conjugate of any Sylow $p$ -subgroup, and the Sylow $p$ -subgroups form a single conjugacy class.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

Let $G$ be finite, let $P$ be a Sylow $p$ -subgroup, and let $H \leq G$ be a $p$ -subgroup. There is $g \in G$ with $H \leq g P g^{- 1}$ . In particular, for every Sylow $p$ -subgroup $Q$ there is $g \in G$ with $Q = g P g^{- 1}$ , so the Sylow $p$ -subgroups form one conjugacy class. (Sylow II: in a finite group every $p$ -subgroup lies in a conjugate of any Sylow $p$ -subgroup, and the Sylow $p$ -subgroups form a single conjugacy class).

[L2]

For a finite group $G$ and a prime $p$ , let ${Syl}_{p} (G)$ be the set of Sylow $p$ -subgroups (def-sylow-p-subgroup). Define $n_{p} (G) : = ∣ {Syl}_{p} (G) ∣ .$ This cardinal is defined even before existence is proved because ${Syl}_{p} (G)$ is a subset of the finite power set of $G$ ; thm-sylow-first-theorem later shows it is nonzero. (The number $n_{p} (G)$ of Sylow $p$ -subgroups).

[L3]

Let $H \leq G$ . The rule $G / N_{G} (H) ⟶ {g H g^{- 1} : g \in G}, g N_{G} (H) ⟼ g H g^{- 1},$ is a well-defined bijection. If $G$ is finite, the number of distinct conjugates of $H$ is $[G : N_{G} (H)]$ . (The conjugates of $H$ are in bijection with $G / N_{G} (H)$ and, for finite $G$ , number $[G : N_{G} (H)]$ ).

Proof

technique · direct

1.1

Conjugation is transitive on the Sylow $p$ -subgroups by Sylow II, and the stabilizer of $P$ is exactly $N_{G} (P)$ .

L1L2L3givenalgebra

2.1

By step 1.1 the set of Sylow $p$ -subgroups is exactly the conjugacy class of $P$ , so [L3] counts it as $[G : N_{G} (P)]$ , and [L2] identifies that count with $n_{p} (G)$ . If $P$ is the unique Sylow $p$ -subgroup, then $N_{G} (P) = G$ and both sides are $1$ ; if $p ∤ ∣ G ∣$ , then $P = {1}$ , again with $N_{G} (P) = G$ and both sides $1$ . This proves the stated claim.

step 1.1L2L3givenalgebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 40 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Keith Conrad, Consequences of the Sylow Theorems, Sections 1-5 (standard reference, not scraped)

Sylow III*: np(G)=[G:NG(P)]np​(G)=[G:NG​(P)]