PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

Three equivalent descriptions of an extraspecial $p$ -group

Statement

For a finite $p$ -group $P$ the following are equivalent: $P$ is extraspecial; $P$ is nonabelian, $∣ Z (P) ∣ = p$ and $P / Z (P)$ is elementary abelian; $P$ is nonabelian and $Z (P) = P^{'} = Φ (P)$ has order $p$ .

Here $P^{'} = [P, P]$ , $Φ (P)$ is the Frattini subgroup, and quotients are those of The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ .

Facts & Assumptions

Given: A prime $p$ and a finite $p$ -group $P$ (A finite $p$ -group has order $p^{n}$ for a prime $p$ and some $n \in N$ ).

[F1]

A finite $p$ -group $P$ is special when $Z (P) = P^{'} = Φ (P)$ is elementary abelian, and extraspecial when in addition $P$ is nonabelian and this common subgroup has order $p$ (Special and extraspecial $p$ -groups).

[L1]

For a finite $p$ -group $P$ , the quotient $P / Φ (P)$ is elementary abelian, and for $N ⊴ P$ the quotient $P / N$ is elementary abelian if and only if $Φ (P) \leq N$ (The Frattini quotient is the largest elementary abelian quotient of a finite $p$ -group).

[L2]

For every finite $p$ -group $P$ , $Φ (P) = P^{'} P^{p}$ , where $P^{p} = ⟨ g^{p} : g \in P ⟩$ ( $Φ (P) = P^{'} P^{p}$ for a finite $p$ -group, The $p$ th-power subgroup $G^{p}$ ).

[L3]

For $N ⊴ G$ , the quotient $G / N$ is abelian if and only if $[G, G] \subseteq N$ ( $G / N$ is abelian if and only if $[G, G] \subseteq N$ ).

[L4]

An elementary abelian $p$ -group is a finite abelian $p$ -group in which every nonidentity element has order $p$ ; the trivial group is permitted (Elementary abelian $p$ -groups).

[L5]

For every group $G$ , the center $Z (G)$ is a normal subgroup of $G$ (The center of a group is a normal subgroup).

[L6]

For a finite group $G$ and $H \leq G$ , $∣ G ∣ = [G : H] ∣ H ∣$ (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

[L7]

In a finite group whose order is prime, every $g \neq e$ has order $∣ G ∣$ and generates $G$ (A finite group of prime order is cyclic and every nonidentity element generates it).

Proof

technique · direct

1.1

Suppose $P$ is extraspecial. Then $P$ is nonabelian, $Φ (P) = Z (P)$ has order $p$ , and $P / Φ (P)$ is elementary abelian; since $Φ (P) = Z (P)$ this says $P / Z (P)$ is elementary abelian, the quotient being formed along a normal subgroup. So the second description holds.

F1L1L4L5

1.2

Suppose $P$ is nonabelian with $∣ Z (P) ∣ = p$ and $P / Z (P)$ elementary abelian. Applying the elementary abelian criterion to the normal subgroup $Z (P)$ gives $Φ (P) \leq Z (P)$ , and an elementary abelian quotient is abelian, so $P^{'} \leq Z (P)$ . As $P$ is nonabelian, $P^{'} \neq 1$ ; a subgroup of the group $Z (P)$ of order $p$ has order $1$ or $p$ , so $P^{'} = Z (P)$ . Then $Φ (P) = P^{'} P^{p}$ contains $P^{'} = Z (P)$ and is contained in $Z (P)$ , so $Φ (P) = P^{'} = Z (P)$ has order $p$ , which is the third description.

L1L2L3L5L6

1.3

Suppose $P$ is nonabelian with $Z (P) = P^{'} = Φ (P)$ of order $p$ . A group of prime order is cyclic, hence abelian, and each of its nonidentity elements has order $p$ , so this common subgroup is elementary abelian; it is a finite $p$ -group because its order is $p$ . Thus $P$ meets the definition and is extraspecial.

F1L4L7

2.1

The three implications close a cycle, so the three descriptions are equivalent.

step 1.1step 1.2step 1.3∎

Remarks

The nonabelian hypothesis does real work exactly once, in step 1.2, where it supplies $P^{'} \neq 1$ . Dropping it leaves the cyclic group of order $p$ satisfying the second description with $Z (P) = P$ of order $p$ and trivial quotient, while its derived subgroup is trivial and the third description fails.

Depends on

Used by

Dependency tree · two levels

50 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

D. A. Craven, The Theory of p-Groups, Definition 3.1 and §2.2 Theorem 2.19 (standard reference, not scraped)
M. van Beek, Topics in Finite p-Groups, Definitions 2.28 and 2.30 (standard reference, not scraped)

Three equivalent descriptions of an extraspecial pp-group