Alphabeta MathHow 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
- For odd p, a direct product of two Heisenberg groups is special with centre of order p², hence not extraspecial Counterexample
- 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
- Order, centre and derived subgroup of a central product Proposition
- A finite abelian group is the internal direct product of its primary components Theorem
- For k≥3, (ℤ/2ᵏℤ)^×≅ C₂× C_2ᵏ⁻², generated uniquely as (-1)^ε5ʲ Theorem
- Fundamental theorem of finite abelian groups: invariant-factor form Theorem
Dependency tree · two levels
23 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
- Sharifi, Abstract Algebra, direct products (standard reference, not scraped)