Alphabeta Math
CorollaryStatement: 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.

An extraspecial group of odd order has exponent p or p2, and an extraspecial 2-group has exponent 4

Statement

Let P be an extraspecial p-group of order p1+2n. If p is odd then exp(P)=p when P is of plus type and exp(P)=p2 when P is of minus type. If p=2 then exp(P)=4, whichever type P is.

Facts & Assumptions

Given: An extraspecial p-group P of order p1+2n with n1.

[F1]

For a finite group G, exp(G)=min{nN:n>0 and gn=e for every gG} (The exponent of a finite group).

[F2]

For odd p, p+1+2n is the extraspecial group of that order with exponent p and p1+2n the one with exponent p2; at p=2 the two are named by their number of solutions of x2=1 (Plus and minus type of an extraspecial p-group).

[F4]

For a group G and a prime p, Gp=gp:gG (The pth-power subgroup Gp).

[L1]

For odd p there are exactly two extraspecial groups of order p1+2n, distinguished by their exponent, which is p for one and p2 for the other (For odd p and each n1 there are exactly two extraspecial groups of order p1+2n, distinguished by their exponent).

[L2]

For each n1 there are exactly two extraspecial groups of order 21+2n, separated by the number of solutions of x2=1 (For each n1 there are exactly two extraspecial groups of order 21+2n).

[L3]

There are n1 subgroups of P, each nonabelian of order p3 with centre Z(P), forming an internal central product of P (Every extraspecial p-group is an internal central product of nonabelian subgroups of order p3).

[L4]

For every prime p there are exactly two nonabelian groups of order p3; at p=2 they are Dih(C4) and Q8 (For each prime there are exactly two nonabelian groups of order p3 up to isomorphism).

[L6]

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

[L7]

For every finite p-group P, Φ(P)=PPp (Φ(P)=PPp for a finite p-group).

Proof

technique · direct
1.1

Every gP has gpPpΦ(P)=Z(P), a group of order p, so gp2=(gp)p=e and exp(P) divides p2.

F1F4L6L7
1.2

For odd p the classification names the two isomorphism classes by their exponents, which are p and p2, and the plus and minus labels are those names.

F2L1
2.1

At p=2, take an internal central product decomposition into subgroups of order eight; each is nonabelian, hence isomorphic to Dih(C4) or to Q8, and each contains an element of order four. So exp(P) is a multiple of four, and by step 1.1 it divides four; hence exp(P)=4 for both types.

F1F3L2L3L4L5step 1.1

Remarks

At p=2 the exponent does not separate the two types, and that is why the classification there uses the number of solutions of x2=1 instead. The two invariants are not interchangeable: for odd p the exponent separates the types and the number of solutions of xp=1 does so as well, while at p=2 only the second does.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

76 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