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.
For finite groups and ,
Statement
If and are finite groups, then their external direct product is finite and has order .
Facts & Assumptions
Given: Finite groups .
The direct product has underlying set and is a group ( is a group with identity , coordinatewise inverses, and homomorphic coordinate projections).
The order of a finite group is the cardinality of its underlying set (The order of a finite group and the order of an element, with when no positive power of is the identity).
The Cartesian product of finite sets has cardinality the product of their cardinalities (The product rule: , and ).
Proof
The carrier of the direct-product group is the Cartesian product of the finite carriers and .
By the finite product rule, is finite and .
Reading these three cardinalities as group orders gives .
Depends on
- $G\times H$ is a group with identity $(e_G,e_H)$, coordinatewise inverses, and homomorphic coordinate projections
- 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
- The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$, and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$
Used by
- Invariant factors determine the order and exponent of a finite abelian group Corollary
- Isomorphism classes of abelian groups of order pⁿ are counted by partitions of n Corollary
- Successive p-multiple layers recover the summands of Cₚ² times C_p³ times C_p⁴² Example
- The successive quotients pⁱG/pⁱ⁺¹G recover the cyclic summand multiplicities of a finite abelian p-group Lemma
- A finite abelian group is the internal direct product of its primary components Theorem
- Fundamental theorem of finite abelian groups: invariant-factor form Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 65 results over 17 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
- Sharifi, Abstract Algebra, direct products (standard reference, not scraped)