CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-16

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.

$(Z / 15 Z)^{\times}$ has order $8$ but is not cyclic

Statement refuted

The order of a unit group need not be the order of one of its elements: $(Z / 15)^{\times}$ has order $8$ but is not cyclic.

Facts & Assumptions

Given: The modulus $15 = 3 \cdot 5$ .

[L1]

The unit-group structure theorem gives the product of the prime-power factors (The unit group modulo $n$ is the product of its odd-prime cyclic factors and its explicit $2$ -power factor).

[L2]

An element of finite order $r$ has its $t$ th power equal to the identity exactly when $r ∣ t$ (If $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 $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ).

Counterexample

technique · direct

1.1L1algebra

By [L1], $(Z / 15)^{\times} ≅ C_{2} \times C_{4}$ , which has $8$ elements.

2.1step 1.1L2algebra∎

For every pair $(x, y) \in C_{2} \times C_{4}$ , [L2] gives $x^{4} = 1$ and $y^{4} = 1$ , so $(x, y)^{4} = (1, 1)$ . Another application of [L2] shows its order divides $4$ . Thus no element has order $8$ and the group is not cyclic.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

William Stein, Elementary Number Theory, §2.5 (standard reference, not scraped)

(Z/15Z)×(Z/15Z)× has order 88 but is not cyclic