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.
The order of a finite group and the order of an element, with when no positive power of is the identity
Definition
The order of a finite group. Let be a group (Group and abelian group) whose underlying set is finite (Finite, countably infinite, countable, uncountable), so that for some (Equinumerous sets, and ). That natural number is unique: if and then , since is symmetric and transitive, and then by claim 3 of The pigeonhole principle on . The order of is that unique natural number, written . A group is infinite when its underlying set is not finite, and is then not defined.
The order of an element. Let be any group and , with natural powers as in Powers : natural exponents in a monoid and integer exponents in a group, with . Put
-
If , the order of is its least element,
which exists by the well-ordering principle (The well-ordering principle): every nonempty subset of has a least element, and that element is unique, being every element of and a member of it. We then say has finite order.
-
If we say has infinite order and write , where is a symbol reserved for this case and is not a natural number. No arithmetic is performed with it here.
By construction whenever it is finite, and exactly when , since .
Every element of a finite group has finite order. If is finite then for every , by In a finite group, every element satisfies for some natural , so is a natural number.
Remarks
-
Two well-definedness obligations, both discharged above and neither parenthetical. For it is that a finite set is equinumerous with exactly one natural number, which is claim 3 of The pigeonhole principle on . For it is that the set has a least element when it is nonempty, which is The well-ordering principle, and that it is nonempty at all in the finite case, which is In a finite group, every element satisfies for some natural . Neither quantity is definable before those three items.
-
and are the same kind of thing, and that is not an accident. If then iff is an integer multiple of , the powers are distinct, and has exactly elements; if has infinite order then only for proves : the order of an element is the order of the group it generates. The shared word and the shared notation are justified by that identity, not by convention.
-
is not a value in , so a statement such as "" is asserted only when the order is finite; the infinite case is always stated separately. The order on used above is the additive one of Order on the natural numbers, and contains (The natural numbers (von Neumann)), which is why carries the condition : holds for every and says nothing.
Depends on
Group and abelian group
Powers : natural exponents in a monoid and integer exponents in a group, with
In a finite group, every element satisfies for some natural
The well-ordering principle
Finite, countably infinite, countable, uncountable
Equinumerous sets, and
The pigeonhole principle on
The natural numbers (von Neumann)
Order on the natural numbers