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 or , and an extraspecial -group has exponent
Statement
Let be an extraspecial -group of order . If is odd then when is of plus type and when is of minus type. If then , whichever type is.
Facts & Assumptions
Given: An extraspecial -group of order with .
For a finite group , (The exponent of a finite group).
For odd , is the extraspecial group of that order with exponent and the one with exponent ; at the two are named by their number of solutions of (Plus and minus type of an extraspecial -group).
For a group and a prime , (The th-power subgroup ).
For odd there are exactly two extraspecial groups of order , distinguished by their exponent, which is for one and for the other (For odd and each there are exactly two extraspecial groups of order , distinguished by their exponent).
For each there are exactly two extraspecial groups of order , separated by the number of solutions of (For each there are exactly two extraspecial groups of order ).
There are subgroups of , each nonabelian of order with centre , forming an internal central product of (Every extraspecial -group is an internal central product of nonabelian subgroups of order ).
For every prime there are exactly two nonabelian groups of order ; at they are and (For each prime there are exactly two nonabelian groups of order up to isomorphism).
In the rotation has order four, and in the element has order four ( and are extraspecial of order , with six and two solutions of respectively, is a subgroup of with eight elements, and is its only element of order ).
For a finite -group the following are equivalent: is extraspecial; is nonabelian, and is elementary abelian; is nonabelian and has order (Three equivalent descriptions of an extraspecial -group).
For every finite -group , ( for a finite -group).
Proof
Every has , a group of order , so and divides .
For odd the classification names the two isomorphism classes by their exponents, which are and , and the plus and minus labels are those names.
At , take an internal central product decomposition into subgroups of order eight; each is nonabelian, hence isomorphic to or to , and each contains an element of order four. So is a multiple of four, and by step 1.1 it divides four; hence for both types.
Remarks
At the exponent does not separate the two types, and that is why the classification there uses the number of solutions of instead. The two invariants are not interchangeable: for odd the exponent separates the types and the number of solutions of does so as well, while at only the second does.
Depends on
- $\operatorname{Dih}(C_4)$ and $Q_8$ are extraspecial of order $8$, with six and two solutions of $x^2=1$ respectively
- $Q_8$ is a subgroup of $\mathbb{H}^{\times}$ with eight elements, and $-1$ is its only element of order $2$
- For each $n\ge1$ there are exactly two extraspecial groups of order $2^{1+2n}$
- For odd $p$ and each $n\ge1$ there are exactly two extraspecial groups of order $p^{1+2n}$, distinguished by their exponent
- For each prime there are exactly two nonabelian groups of order $p^3$ up to isomorphism
- Every extraspecial $p$-group is an internal central product of nonabelian subgroups of order $p^3$
- Three equivalent descriptions of an extraspecial $p$-group
- $\Phi(P)=P'P^p$ for a finite $p$-group
- The $p$th-power subgroup $G^p$
- Plus and minus type of an extraspecial $p$-group
- The exponent of a finite group
- The order $|G|$ of a finite group and the order $\operatorname{ord}(g)$ of an element, with $\operatorname{ord}(g) = \infty$ when no positive power of $g$ is the identity
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
- M. van Beek, Topics in Finite p-Groups, Proposition 2.39(iii) (standard reference, not scraped)