Description: Factorization of a finite abelian p-group. There is a direct product decomposition of any abelian group of prime-power order where one of the factors is cyclic and generated by an element of maximal order. (Contributed by Mario Carneiro, 27-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pgpfac1.k | |
|
pgpfac1.s | |
||
pgpfac1.b | |
||
pgpfac1.o | |
||
pgpfac1.e | |
||
pgpfac1.z | |
||
pgpfac1.l | |
||
pgpfac1.p | |
||
pgpfac1.g | |
||
pgpfac1.n | |
||
pgpfac1.oe | |
||
pgpfac1.ab | |
||
Assertion | pgpfac1 | |