LemmaStatement: 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.

Two elements of an extraspecial $p$ -group with nontrivial commutator generate an extraspecial subgroup of order $p^{3}$

Statement

Let $P$ be an extraspecial $p$ -group with $Z (P) = ⟨ z ⟩$ , and let $x, y \in P$ satisfy $[x, y] \neq e$ . Then $Q = ⟨ x, y ⟩$ contains $Z (P)$ , has order $p^{3}$ , is nonabelian, and is extraspecial with $Z (Q) = Z (P)$ .

Facts & Assumptions

Given: An extraspecial $p$ -group $P$ with $Z (P) = ⟨ z ⟩$ of order $p$ , the quotient $V = P / Z (P)$ with its commutator pairing $b_{z}$ , and elements $x, y \in P$ with $[x, y] \neq e$ .

[F1]

The commutator pairing of $P$ relative to $z$ is the map $b_{z} : V \times V \to F_{p}$ determined by $[x, y] = z^{b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y})}$ (The commutator pairing of an extraspecial $p$ -group relative to a chosen generator of its centre).

[F2]

$Z (G) : = {z \in G : z g = g z for every g \in G}$ (The center $Z (G)$ of a group).

[F3]

A subset $S$ of an elementary abelian $p$ -group is independent when $\prod_{s \in S} s^{a_{s}} = e$ with finite support forces every $a_{s} = 0$ , and it spans when every element is such a product ( $F_{p}$ -spanning sets, independence, and bases in an elementary abelian $p$ -group).

[F4]

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

[L1]

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$ (Three equivalent descriptions of an extraspecial $p$ -group).

[L2]

The commutator pairing is well defined, $F_{p}$ -bilinear and alternating, and satisfies $b_{z} (\overset{ˉ}{y}, \overset{ˉ}{x}) = - b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y})$ (The commutator pairing is well defined on the central quotient, is bilinear over $F_{p}$ , and is alternating).

[L3]

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).

[L4]

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$ ).

[L5]

If the quotient group $G / Z (G)$ is cyclic, then $G$ is abelian (If $G / Z (G)$ is cyclic, then $G$ is abelian).

[L6]

$⟨ S ⟩$ is the smallest subgroup of $G$ containing $S$ (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[L7]

The rule $\overset{ˉ}{a} \cdot x = x^{a}$ gives every elementary abelian $p$ -group its canonical $F_{p}$ -vector-space structure (An elementary abelian $p$ -group has a canonical $F_{p}$ -vector-space structure).

[L8]

If $P$ is a finite $p$ -group and $H \leq P$ , then $∣ H ∣ = p^{k}$ for some $k \in N$ (Every subgroup of a finite $p$ -group has order a power of $p$ ).

Proof

technique · direct

1.1

The element $[x, y]$ lies in $[P, P] = Z (P)$ and is not the identity, so it generates the group $Z (P)$ of order $p$ ; since $[x, y] \in Q$ , this gives $Z (P) \leq Q$ .

F2L1L3L6

1.2

Write $c = b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y})$ ; then $z^{c} = [x, y] \neq e$ , so $c \neq 0$ in $F_{p}$ .

2.1

The pair $\overset{ˉ}{x}, \overset{ˉ}{y}$ is independent in $V$ : if ${\overset{ˉ}{x}}^{a} {\overset{ˉ}{y}}^{d}$ is the identity of $V$ , pairing with $\overset{ˉ}{y}$ gives $a c = 0$ and hence $a = 0$ , and pairing with $\overset{ˉ}{x}$ gives $- d c = 0$ and hence $d = 0$ .

F3L2L7step 1.2

3.1

Since $Z (P) \leq Q$ , the image of $Q$ in $V$ is $Q / Z (P)$ , and it equals $⟨ \overset{ˉ}{x}, \overset{ˉ}{y} ⟩ = {{\overset{ˉ}{x}}^{a} {\overset{ˉ}{y}}^{d} : a, d \in F_{p}}$ ; independence makes the $p^{2}$ displayed products pairwise distinct, so $∣ Q / Z (P) ∣ = p^{2}$ and Lagrange gives $∣ Q ∣ = p \cdot p^{2} = p^{3}$ .

F3L4L6L7step 1.1step 2.1

4.1

$Q$ is nonabelian because $[x, y] \neq e$ , and $Z (P) \leq Z (Q)$ because an element central in $P$ is central in the subgroup $Q$ containing it. The order of $Z (Q)$ is a power of $p$ dividing $p^{3}$ and is not $p^{3}$ ; were it $p^{2}$ , the quotient $Q / Z (Q)$ would have order $p$ and hence be cyclic, forcing $Q$ abelian. So $∣ Z (Q) ∣ = p$ and $Z (Q) = Z (P)$ .

F2L3L4L5L8step 1.1step 3.1

5.1

The quotient $Q / Z (Q) = Q / Z (P)$ is a subgroup of the elementary abelian group $V$ , hence is itself a finite abelian $p$ -group all of whose nonidentity elements have order $p$ ; so $Q$ is a nonabelian finite $p$ -group with centre of order $p$ and elementary abelian central quotient, and the characterisation makes it extraspecial.

F4L1step 3.1step 4.1∎

Remarks

The hypothesis is on the pair, not on either element separately: $x$ and $y$ are automatically noncentral, since a central element commutes with everything, but two noncentral elements can commute and then generate an abelian subgroup.

Depends on

Used by

Dependency tree · two levels

51 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, §3.2, proof of Theorem 3.9 (standard reference, not scraped)
M. van Beek, Topics in Finite p-Groups, Theorem 2.40(iii) (standard reference, not scraped)

Two elements of an extraspecial pp-group with nontrivial commutator generate an extraspecial subgroup of order p3p3