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.

✓ 5 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Cyclic Groups and Direct Products

1 · Prerequisites

2 · Summary

The earlier development of groups, subgroups, element orders, and homomorphisms provides the language used here. Cyclic subgroups are already available, while least common multiples and the integer classification of finite cyclic groups support the order calculations and structural identifications.

This page defines the external direct product and proves that it is a group. It computes the size of a finite product and the order of a pair, classifies cyclic groups as either infinite cyclic or finite cyclic, and proves that every subgroup of a cyclic group is cyclic.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-03Open item page →

The external direct product $G \times H$ with componentwise multiplication

Definition

Let $G$ and $H$ be groups. Their external direct product has underlying set

$G \times H : = {(g, h) : g \in G, h \in H}$

and componentwise operation

$(g, h) (g^{'}, h^{'}) : = (g g^{'}, h h^{'}) .$

The fact that this operation makes $G \times H$ a group, with the indicated identity and inverses, is proved in $G \times H$ is a group with identity $(e_{G}, e_{H})$ , coordinatewise inverses, and homomorphic coordinate projections ↗. Until that result is used, this definition introduces only the set and its componentwise binary operation.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

$G \times H$ is a group with identity $(e_{G}, e_{H})$ , coordinatewise inverses, and homomorphic coordinate projections

Statement

For groups $G$ and $H$ , the componentwise operation of The external direct product $G \times H$ with componentwise multiplication makes $G \times H$ a group. Its identity is $(e_{G}, e_{H})$ , and

$(g, h)^{- 1} = (g^{- 1}, h^{- 1}) .$

Moreover the coordinate maps $π_{G} (g, h) = g$ and $π_{H} (g, h) = h$ are group homomorphisms.

Facts & Assumptions

Given: Groups $G, H$ with identities $e_{G}, e_{H}$ .

[L1]

$G \times H$ has the componentwise operation $(g, h) (g^{'}, h^{'}) = (g g^{'}, h h^{'})$ (The external direct product $G \times H$ with componentwise multiplication).

[L2]

A group operation is associative, has a two-sided identity, and gives every element a two-sided inverse (Group and abelian group).

[L3]

A map between groups is a group homomorphism exactly when it preserves products (Monoid homomorphism and group homomorphism).

Proof

technique · direct

1.1

For $(g, h), (g^{'}, h^{'}), (g^{''}, h^{''}) \in G \times H$ , associativity in each factor gives $((g, h) (g^{'}, h^{'})) (g^{''}, h^{''}) = (g g^{'} g^{''}, h h^{'} h^{''}) = (g, h) ((g^{'}, h^{'}) (g^{''}, h^{''}))$ ; thus the componentwise operation is associative.

L1L2givenalgebra

1.2

For every $(g, h) \in G \times H$ , $(e_{G}, e_{H}) (g, h) = (g, h) = (g, h) (e_{G}, e_{H})$ ; thus $(e_{G}, e_{H})$ is a two-sided identity.

L1L2givenalgebra

1.3

For every $(g, h) \in G \times H$ , $(g, h) (g^{- 1}, h^{- 1}) = (e_{G}, e_{H}) = (g^{- 1}, h^{- 1}) (g, h)$ ; so $(g^{- 1}, h^{- 1})$ is its inverse.

L1L2givenalgebra

2.1

Steps 1.1–1.3 verify the group axioms for $G \times H$ .

step 1.1step 1.2step 1.3L2

3.1

For pairs $(g, h), (g^{'}, h^{'})$ , $π_{G} ((g, h) (g^{'}, h^{'})) = g g^{'} = π_{G} (g, h) π_{G} (g^{'}, h^{'})$ ; the same coordinatewise calculation holds for $π_{H}$ , so both projections are homomorphisms from the group in step 2.1.

step 2.1L1L3givenalgebra

4.1

The stated identity, inverse formula, and coordinate homomorphisms follow.

step 2.1step 3.1∎

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

For finite groups $G$ and $H$ , $∣ G \times H ∣ = ∣ G ∣ ∣ H ∣$

Statement

If $G$ and $H$ are finite groups, then their external direct product is finite and has order $∣ G \times H ∣ = ∣ G ∣ ∣ H ∣$ .

Facts & Assumptions

Given: Finite groups $G, H$ .

[L1]

The direct product has underlying set $G \times H$ and is a group ( $G \times H$ is a group with identity $(e_{G}, e_{H})$ , coordinatewise inverses, and homomorphic coordinate projections).

[L2]

The order of a finite group is the cardinality of its underlying set (The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity).

[L3]

The Cartesian product of finite sets has cardinality the product of their cardinalities (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ).

Proof

technique · direct

1.1

The carrier of the direct-product group is the Cartesian product of the finite carriers $G$ and $H$ .

L1given

2.1

By the finite product rule, $G \times H$ is finite and $∣ G \times H ∣_{s e t} = ∣ G ∣_{s e t} ∣ H ∣_{s e t}$ .

step 1.1L3

3.1

Reading these three cardinalities as group orders gives $∣ G \times H ∣ = ∣ G ∣ ∣ H ∣$ .

step 2.1L2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

If $g$ and $h$ have finite orders $m$ and $n$ , then $ι (ord (g, h)) = lcm (ι (m), ι (n))$ in $G \times H$

Statement

Let $ι : N \to Z$ be the canonical embedding. If $g \in G$ and $h \in H$ have finite orders $m, n \geq 1$ , then in the external direct product

$ι (ord (g, h)) = lcm (ι (m), ι (n)) .$

Facts & Assumptions

Given: Groups $G, H$ , elements $g \in G, h \in H$ , and positive natural numbers $m, n$ with $ord (g) = m$ and $ord (h) = n$ .

[L1]

The direct product is a group with componentwise multiplication ( $G \times H$ is a group with identity $(e_{G}, e_{H})$ , coordinatewise inverses, and homomorphic coordinate projections).

[L2]

If an element has finite order $r$ , then for every natural $k$ its $k$ th power is the identity exactly when $ι (r) ∣ ι (k)$ ; equivalently, $r$ is the least positive natural exponent taking it to the identity (The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity, 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$ ).

[L3]

For positive $m, n$ , the integer $L = lcm (ι (m), ι (n))$ is a positive common multiple of $ι (m)$ and $ι (n)$ , and it divides every common multiple. Thus $L = ι (ℓ)$ for a unique natural $ℓ \geq 1$ (Common multiple, and the least common multiple $lcm (a, b)$ , taken to be $0$ when $a = 0$ or $b = 0$ , Every common multiple of $a$ and $b$ is a multiple of $lcm (a, b)$ , and $\gcd (a, b) \cdot lcm (a, b) = ∣ a b ∣$ , The naturals embed in the integers).

[L4]

Induction is valid for natural-number powers (The principle of mathematical induction).

Proof

technique · direct

1.1

For every natural $k$ , $(g, h)^{k} = (g^{k}, h^{k})$ : it holds at $k = 0$ , and the successor step follows by componentwise multiplication.

L1L4given

2.1

Let $ℓ$ be the natural from [L3]. Since $ι (m) ∣ ι (ℓ)$ and $ι (n) ∣ ι (ℓ)$ , [L2] and step 1.1 give $(g, h)^{ℓ} = (e_{G}, e_{H})$ .

step 1.1L2L3given

2.2

If $(g, h)^{k} = (e_{G}, e_{H})$ for a positive natural $k$ , then step 1.1 gives $g^{k} = e_{G}$ and $h^{k} = e_{H}$ . Hence $ι (m) ∣ ι (k)$ and $ι (n) ∣ ι (k)$ .

step 1.1L2given

3.1

By [L3], the two divisibilities of step 2.2 imply $ι (ℓ) ∣ ι (k)$ . As $ℓ, k \geq 1$ , this forces $ℓ \leq k$ : an integer quotient $q$ with $ι (k) = q ι (ℓ)$ is positive and hence at least $1$ . Thus $ℓ$ is the least positive exponent sending $(g, h)$ to the identity.

step 2.1step 2.2L3algebra

4.1

The definition of element order gives $ord (g, h) = ℓ$ . Applying $ι$ and using [L3] gives the displayed equality.

step 3.1L2L3∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Every cyclic group is isomorphic to $(Z, +)$ or to $(Z / n, +)$ for its finite order $n \geq 1$

Statement

If $G = ⟨ g ⟩$ is cyclic, then exactly one of the following applies:

if $g$ has infinite order, $G ≅ (Z, +)$ ;
if $g$ has finite order $n$ , necessarily $n \geq 1$ , then $G ≅ (Z / n, +)$ .

Facts & Assumptions

Given: A group $G$ and an element $g \in G$ with $G = ⟨ g ⟩$ .

[L1]

A cyclic subgroup is precisely the set of all integer powers of its generator ( $⟨ g ⟩ = {g^{n} : n \in Z}$ , and every cyclic group is abelian).

[L2]

For finite order $n$ , $g^{k} = e$ exactly when $n ∣ k$ , while for infinite order no nonzero integer power of $g$ is the identity (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$ ).

[L3]

Integer powers satisfy $g^{r + s} = g^{r} g^{s}$ and $g^{- s} = (g^{s})^{- 1}$ ; a bijective group homomorphism is a group isomorphism (Exponent laws in a group: $g^{m + n} = g^{m} g^{n}$ and $(g^{m})^{n} = g^{m n}$ for all $m, n \in Z$ , and $(g h)^{n} = g^{n} h^{n}$ when $g$ and $h$ commute, Group isomorphisms, automorphisms and the set $Aut (G)$ ).

[L4]

The additive quotient group $(Z, +) / n Z$ is the group $(Z / n, +)$ (For every $n \in N$ , the congruence-class group $(Z / n, +)$ is the quotient group $(Z, +) / n Z$ ).

Proof

technique · direct

1.1

Suppose first that $g$ has infinite order. The map $ϕ : Z \to G$ , $r \mapsto g^{r}$ , is a homomorphism by the power law in [L3]. If $g^{r} = g^{s}$ , then $g^{r - s} = g^{r} (g^{s})^{- 1} = e$ by [L3], so [L2] forces $r = s$ ; it is surjective by [L1].

L1L2L3given

1.2

Suppose instead that $g$ has finite order $n$ . Then $n \geq 1$ by the definition of element order, and $[r] \mapsto g^{r}$ defines a map $\overset{ˉ}{ϕ} : Z / n \to G$ because $[r] = [s]$ means $n ∣ (r - s)$ , so [L2] gives $g^{r - s} = e$ and [L3] gives $g^{r} = g^{r - s} g^{s} = g^{s}$ .

L2L3L4given

2.1

Hence in the infinite-order case $ϕ$ is an isomorphism $Z ≅ G$ .

step 1.1L3

2.2

The map $\overset{ˉ}{ϕ}$ is a homomorphism by the power law, is injective because $g^{r} = g^{s}$ gives $g^{r - s} = g^{r} (g^{s})^{- 1} = e$ by [L3] and then [L2] gives $n ∣ (r - s)$ , and is surjective by [L1].

step 1.2L1L2L3

3.1

Thus $\overset{ˉ}{ϕ}$ is an isomorphism $(Z / n, +) ≅ G$ in the finite-order case.

step 2.2L3L4

4.1

Steps 2.1 and 3.1 give the asserted classification according as the order of $g$ is infinite or finite.

step 2.1step 3.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Every subgroup of a cyclic group is cyclic; the least positive exponent in a nontrivial subgroup supplies a generator

Statement

Every subgroup $H$ of a cyclic group $G = ⟨ g ⟩$ is cyclic. If $H \neq {e}$ , then the least positive integer $d$ for which $g^{d} \in H$ satisfies $H = ⟨ g^{d} ⟩$ .

Facts & Assumptions

Given: A cyclic group $G = ⟨ g ⟩$ and a subgroup $H \leq G$ .

[L1]

A subgroup contains the identity and is closed under products and inverses (Subgroup).

[L2]

The elements of $⟨ g ⟩$ are exactly the integer powers of $g$ , and a subgroup containing one element contains the subgroup generated by it ( $⟨ g ⟩ = {g^{n} : n \in Z}$ , and every cyclic group is abelian, The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[L3]

Integer powers satisfy $g^{r + s} = g^{r} g^{s}$ , $(g^{r})^{- 1} = g^{- r}$ , and $(g^{d})^{q} = g^{d q}$ (Exponent laws in a group: $g^{m + n} = g^{m} g^{n}$ and $(g^{m})^{n} = g^{m n}$ for all $m, n \in Z$ , and $(g h)^{n} = g^{n} h^{n}$ when $g$ and $h$ commute).

[L4]

A nonempty subset of $N$ has a least element (The well-ordering principle).

[L5]

For $d > 0$ and $k \in Z$ , there are $q, r \in Z$ with $k = q d + r$ and $0 \leq r < d$ (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$ ).

[L6]

A nonzero integer is positive or has positive negative (The integers form a totally ordered ring).

Proof

technique · direct

1.1

If $H = {e}$ , then $H = ⟨ e ⟩$ and is cyclic. Assume henceforth that $H \neq {e}$ .

L1L2given

1.2

The set $S : = {n \in N : n \geq 1 and g^{n} \in H}$ is nonempty: choose $h \in H ∖ {e}$ and write $h = g^{k}$ by [L2]. Since $g^{0} = e$ , $k \neq 0$ ; by [L6], either $k > 0$ or $- k > 0$ . In the first case use $h$ , and in the second use $h^{- 1} = g^{- k}$ .

L1L2L3L6given

2.1

Let $d$ be the least element of $S$ , supplied by [L4]. Then $g^{d} \in H$ , so $⟨ g^{d} ⟩ \subseteq H$ by the smallest-subgroup property in [L2].

step 1.2L2L4

3.1

For $h \in H$ , write $h = g^{k}$ by [L2] and write $k = q d + r$ with $0 \leq r < d$ by [L5]. Then $g^{r} = h (g^{d})^{- q} \in H$ .

step 2.1L1L2L3L5

4.1

If $r > 0$ in step 3.1, then $r \in S$ contradicts the minimality of $d$ ; hence $r = 0$ , so $h = (g^{d})^{q} \in ⟨ g^{d} ⟩$ .

step 3.1L2L4

5.1

Thus $H \subseteq ⟨ g^{d} ⟩$ in the nontrivial case, and step 2.1 gives equality; together with step 1.1 this proves every subgroup of $G$ is cyclic.

step 1.1step 2.1step 4.1∎

5 · Examples, counterexamples and false statements

None yet.

Cyclic Groups and Direct Products

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

The external direct product G×HG×H with componentwise multiplication

Definition

G×HG×H is a group with identity (eG,eH)(eG​,eH​), coordinatewise inverses, and homomorphic coordinate projections

Statement

Facts & Assumptions

Proof

For finite groups GG and HH, ∣G×H∣=∣G∣ ∣H∣∣G×H∣=∣G∣∣H∣

Statement

Facts & Assumptions

Proof

If gg and hh have finite orders mm and nn, then ι(ord⁡(g,h))=lcm⁡(ι(m),ι(n))ι(ord(g,h))=lcm(ι(m),ι(n)) in G×HG×H

Statement

Facts & Assumptions

Proof

Every cyclic group is isomorphic to (Z,+)(Z,+) or to (Z/n,+)(Z/n,+) for its finite order n≥1n≥1

Statement

Facts & Assumptions

Proof

Every subgroup of a cyclic group is cyclic; the least positive exponent in a nontrivial subgroup supplies a generator

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources

The external direct product $G \times H$ with componentwise multiplication

$G \times H$ is a group with identity $(e_{G}, e_{H})$ , coordinatewise inverses, and homomorphic coordinate projections

For finite groups $G$ and $H$ , $∣ G \times H ∣ = ∣ G ∣ ∣ H ∣$

If $g$ and $h$ have finite orders $m$ and $n$ , then $ι (ord (g, h)) = lcm (ι (m), ι (n))$ in $G \times H$

Every cyclic group is isomorphic to $(Z, +)$ or to $(Z / n, +)$ for its finite order $n \geq 1$