ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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} = (Z / 2, +) \times (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 $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 $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ , For every $n \in N$ , the congruence-class group $(Z / n, +)$ is the quotient group $(Z, +) / n Z$ , For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold, Addition and multiplication on $Z / n$ by $[a]_{n} + [b]_{n} = [a + b]_{n}$ and $[a]_{n} [b]_{n} = [a b]_{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 $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$ ).

Verification

technique · direct

1.1

Dividing any integer $a$ by $2$ gives $a = 2 q + r$ with $0 \leq 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 · two levels

41 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

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

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