ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03

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 Klein four-group as the direct product of two groups of order $2$

Example

The Klein four-group is

$V_4=(\mathbb Z/2,+)\times(\mathbb Z/2,+).$

It has the four elements $(0,0),(1,0),(0,1),(1,1)$ . Every nonidentity element has order $2$ , so $V_4$ is not cyclic.

Facts & Assumptions

Given: The residue-class additive group $\mathbb Z/2$ .

[L1]

Division with remainder is available in the integers, and congruence classes modulo $2$ are the quotient group with its stated addition and identity class $0$ (Division with remainder in $\mathbb{Z}$ : for $a \in \mathbb{Z}$ and $b > 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < b$ , For every $n\in\mathbb N$ , the congruence-class group $(\mathbb Z/n,+)$ is the quotient group $(\mathbb Z,+)/n\mathbb Z$ , For every natural $n$ , $(\mathbb{Z}/n,+)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold, Addition and multiplication on $\mathbb{Z}/n$ by $[a]_n+[b]_n=[a+b]_n$ and $[a]_n[b]_n=[ab]_n$ ).

[L2]

The external direct product of two groups is a group with componentwise operation ( $G\times H$ is a group with identity $(e_G,e_H)$ , coordinatewise inverses, and homomorphic coordinate projections).

[L3]

If an element has finite order, then the cyclic subgroup it generates has that many elements (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$ ).

Verification

technique · direct

1.1

Dividing any integer $a$ by $2$ gives $a=2q+r$ with $0\le r<2$ , so its class is either $[0]$ or $[1]$ . These are distinct because $1-0$ is not a multiple of $2$ , and $[1]+[1]=[0]$ . Hence the four displayed pairs are exactly the elements of $V_4$ .

L1givenalgebra

2.1

For each nonzero pair $(a,b)$ in that list, $(a,b)+(a,b)=(a+a,b+b)=(0,0)$ ; it is not the identity, so its order is $2$ .

step 1.1L2algebra

3.1

If $V_4$ were cyclic, a generator could not be the identity, so step 2.1 would give it order $2$ . Then [L3] says that its cyclic subgroup has two elements, contradicting step 1.1. Thus $V_4$ is not cyclic.

step 1.1step 2.1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 84 results over 23 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

Judson, Abstract Algebra: direct products of groups (standard reference, not scraped)

The Klein four-group as the direct product of two groups of order 222