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.
Every group of order , for prime , is abelian
Statement
If is prime and is a group of order , then is abelian.
Facts & Assumptions
Given: A prime and a finite group with .
A nontrivial finite -group has nontrivial center (Every nontrivial finite -group has nontrivial center, in fact divides ).
If is cyclic, then is abelian (If is cyclic, then is abelian).
For finite , (If is finite then ; for finite this equals ).
A group of prime order is cyclic (A finite group of prime order is cyclic and every nonidentity element generates it).
A group of order is a finite -group (A finite -group has order for a prime and some ).
Every subgroup of a finite -group has prime-power order (Every subgroup of a finite -group has order a power of ).
The center is a normal subgroup, hence in particular a subgroup, of (The center of a group is a normal subgroup).
A finite subset with the same cardinality as its ambient finite set is the whole set (A subset of a finite set is finite, with , and equality holds if and only if ).
Proof
By [L1] and [L7], is a nontrivial subgroup of ; [L5] and [L6] therefore show that it has order or .
If , then [L8] gives , so is abelian. If , then [L3] gives , so [L4] makes cyclic.
In the second case [L2] makes abelian, and the first case already did so. Hence every group of order is abelian.
Depends on
- Every nontrivial finite $p$-group has nontrivial center, in fact $p$ divides $|Z(P)|$
- If $G/Z(G)$ is cyclic, then $G$ is abelian
- If $[G:N]$ is finite then $|G/N|=[G:N]$; for finite $G$ this equals $|G|/|N|$
- A finite group of prime order is cyclic and every nonidentity element generates it
- A finite $p$-group has order $p^n$ for a prime $p$ and some $n\in\mathbb N$
- Every subgroup of a finite $p$-group has order a power of $p$
- The center of a group is a normal subgroup
- A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$, and equality holds if and only if $B = A$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 122 results over 26 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- K. Conrad, Group Actions, Corollary 5.2 (standard reference, not scraped)