CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-01

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 every element of a finite group divides the order of the group

Statement

If $G$ is finite and $g\in G$ , then $g$ has finite order and

$\iota(\operatorname{ord}(g))\mid\iota(|G|)$

in $\mathbb Z$ , where $\iota:\mathbb N\to\mathbb Z$ is the canonical embedding.

Facts & Assumptions

Given: A finite group $G$ and an element $g\in G$ .

[F1]

The generated set $\langle g\rangle$ is a subgroup of $G$ and equals the set of integer powers of $g$ (The subgroup $\langle S \rangle$ generated by a subset, the cyclic subgroup $\langle g \rangle$ , and cyclic groups, $\langle g \rangle = \{\, g^{n} : n \in \mathbb{Z} \,\}$ , and every cyclic group is abelian).

[L1]

If $g$ has finite order, then $\langle g\rangle$ is finite and $|\langle g\rangle|=\operatorname{ord}(g)$ ; every element of a finite group has finite order (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).

[L2]

Lagrange's theorem gives $|G|=[G:H]|H|$ for every subgroup $H$ of a finite group and consequently $\iota(|H|)\mid\iota(|G|)$ (Lagrange's theorem: $|G|=[G:H]|H|$ for every subgroup $H$ of a finite group $G$ , Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ , The naturals embed in the integers).

Proof

technique · direct

1.1

The element $g$ has finite order, and $\langle g\rangle\le G$ has order $|\langle g\rangle|=\operatorname{ord}(g)$ .

F1L1

2.1

Apply [L2] to $H=\langle g\rangle$ to obtain $\iota(\operatorname{ord}(g))\mid\iota(|G|)$ .

step 1.1L2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 86 results over 18 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, Cosets and 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)