CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11

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.

Every subgroup of index $p$ in a finite $p$ -group is normal

Statement

Let $P$ be a finite $p$ -group and let $H \leq P$ . If $[P : H] = p$ , then $H ⊴ P$ .

Facts & Assumptions

Given: A finite $p$ -group $P$ and a subgroup $H \leq P$ with $[P : H] = p$ .

[L1]

For $K = {Core}_{P} (H)$ , one has $K ⊴ P$ , $K \leq H$ , and $[P : K] ∣ p!$ (If $[G : H] = n < \infty$ , then ${Core}_{G} (H) ⊴ G$ , $[G : {Core}_{G} (H)] ∣ n!$ , and only finitely many subgroups contain $H$ , ${Core}_{G} (H)$ is the largest normal subgroup of $G$ contained in $H$ ).

[L2]

Every subgroup of $P$ has order a power of $p$ (Every subgroup of a finite $p$ -group has order a power of $p$ ).

[L3]

If $K \leq H \leq P$ , then $[P : K] = [P : H] [H : K]$ (For $K \leq H \leq G$ with $G$ finite, $[G : K] = [G : H] [H : K]$ ).

[L4]

The factorial is the product of the positive natural numbers at most $p$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[L5]

If a prime divides a finite product, it divides one of the factors (If a prime $p$ divides a finite product $\prod_{i < n} a_{i}$ of integers then $p ∣ a_{i}$ for some $i < n$ ; at $n = 0$ the product is $1$ and the hypothesis cannot hold).

[L6]

Prime factorisation is unique (For $n \geq 1$ and any injective list $p : r \to Z$ of primes containing every prime divisor of $n$ , one has $n = \prod_{i < r} p_{i}^{v_{p_{i}} (n)}$ ; the exponents are determined by $n$ , and $v_{q} (n) = 0$ for every prime $q$ outside the list).

[L7]

A prime $p$ is greater than $1$ and has no positive divisors other than $1$ and $p$ (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L8]

For a subgroup of a finite group, the subgroup order divides the group order and the quotient is the index (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

Proof

technique · direct

1.1

Put $K = {Core}_{P} (H)$ . By [L1] and [L3], $K ⊴ P$ , $K \leq H$ , $[P : K] ∣ p!$ , and $[P : K] = p [H : K]$ .

L1L3

2.1

By [L2] and [L8], the orders of $P$ and $K$ are powers of $p$ and their quotient is $[P : K]$ ; [L6] therefore makes $[P : K]$ a positive power of $p$ , and step 1.1 makes it divisible by $p$ .

step 1.1L2L6L8

3.1

Among the factors $1, \dots, p$ in $p!$ , only $p$ is divisible by $p$ by [L7]. If $p^{2}$ divided $p!$ , cancellation of the factor $p$ and [L5] would make $p$ divide one of $1, \dots, p - 1$ , impossible. Thus the positive power of $p$ in step 2.1 that divides $p!$ is exactly $p$ .

step 1.1step 2.1L4L5L7

4.1

Step 1.1 now gives $p = p [H : K]$ , so $[H : K] = 1$ and $H = K$ . Since $K$ is normal in $P$ , so is $H$ .

step 1.1step 3.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

79 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

K. Conrad, Group Actions, Corollary 6.4 (standard reference, not scraped)

Every subgroup of index pp in a finite pp-group is normal