External Direct Product
Let be a finite collection of groups. The external direct product of , written as , is the set of all -tuples for which the th component is an element of and the operation is componentwise. In symbols,
The External Direct Product With Componentwise Multiplication Is a Group
Let be a direct propduct, where we define multiplication as
It is understood that each product is performed with the operation of , then this forms a group
TODO: Add the proof here.
Note that in the case that each is finite, we have by properties of sets that .