CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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\le P$ . If $[P:H]=p$ , then $H\mathrel{\trianglelefteq}P$ .

Facts & Assumptions

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

[L1]

For $K=\operatorname{Core}_P(H)$ , one has $K\mathrel{\trianglelefteq}P$ , $K\le H$ , and $[P:K]\mid p!$ (If $[G:H]=n<\infty$ , then $\operatorname{Core}_G(H)\trianglelefteq G$ , $[G:\operatorname{Core}_G(H)]\mid n!$ , and only finitely many subgroups contain $H$ , $\operatorname{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\le H\le P$ , then $[P:K]=[P:H][H:K]$ (For $K\le H\le 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 $\mathbb{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 \mid 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 \ge 1$ and any injective list $p : r \to \mathbb{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=\operatorname{Core}_P(H)$ . By [L1] and [L3], $K\mathrel{\trianglelefteq}P$ , $K\le H$ , $[P:K]\mid 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,\ldots,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,\ldots,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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 148 results over 27 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

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

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