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.
for every element of a finite group
Statement
Let be a finite group with identity . Then
for every .
Facts & Assumptions
Given: A finite group with identity and an element .
If , then for every integer , if and only if (If then iff is an integer multiple of , the powers are distinct, and has exactly elements; if has infinite order then only for , Powers : natural exponents in a monoid and integer exponents in a group, with , Exponent laws in a group: and for all , and when and commute).
Proof
By [L1], divides after both naturals are embedded in .
Applying [L2] with gives .
Depends on
- The order of every element of a finite group divides the order of the group
- If $\operatorname{ord}(g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$, the powers $g^{0}, \dots, g^{n-1}$ are distinct, and $\langle g \rangle$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$
- 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
- Powers $g^{n}$: natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$
- Exponent laws in a group: $g^{m+n} = g^{m}g^{n}$ and $(g^{m})^{n} = g^{mn}$ for all $m, n \in \mathbb{Z}$, and $(gh)^{n} = g^{n}h^{n}$ **when $g$ and $h$ commute**
- The naturals embed in the integers
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 76 results over 21 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
- Thomas W. Judson, Abstract Algebra: Theory and Applications, Lagrange's Theorem (standard reference, not scraped)
- Thomas W. Judson, Abstract Algebra: Theory and Applications, §6.2: Lagrange's Theorem (standard reference, not scraped)
- Thomas W. Judson, Abstract Algebra: Theory and Applications, §4.1: Cyclic Subgroups (standard reference, not scraped)