LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04

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.

A normal Hall subgroup presents the ambient group as an extension of coprime orders

Statement

Let $N ⊴ G$ be a normal Hall $π$ -subgroup of a finite group $G$ . Then

$1 \to N \to G \to G / N \to 1$

is a group extension with $\gcd (∣ N ∣, ∣ G / N ∣) = 1$ .

Facts & Assumptions

Given: A finite group $G$ and a normal Hall $π$ -subgroup $N ⊴ G$ .

[L1]

A Hall $π$ -subgroup has order coprime to its index (Hall pi-subgroup).

[L2]

For a finite group, the order of a quotient is the index of the kernel (If $[G : N]$ is finite then $∣ G / N ∣ = [G : N]$ ; for finite $G$ this equals $∣ G ∣ / ∣ N ∣$ ).

[L3]

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

Proof

technique · direct

1.1givenL1

Because $N$ is a Hall $π$ -subgroup, [L1] gives $\gcd (∣ N ∣, [G : N]) = 1$ .

2.1L2L3step 1.1∎

Since $N ⊴ G$ , the quotient $G / N$ exists and [L2] gives $∣ G / N ∣ = [G : N]$ . Therefore step 1.1 says exactly that $\gcd (∣ N ∣, ∣ G / N ∣) = 1$ . The displayed short exact sequence is the standard quotient extension.

Depends on

Used by

Schur-Zassenhaus existence theorem Theorem

Dependency tree · two levels

14 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

David A. Craven, Finite Group Theory (standard reference, not scraped)