Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11
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.

The number of finite abelian groups of order n is the product of the partition numbers of the prime exponents of n

Statement

Let n≥1, and write its canonical prime factorisation as n=∏i<rpiai, with the pi distinct and ai>0. Then the number of isomorphism classes of abelian groups of order n is ∏i<rP(ai), where P(a) is the number of partitions of a. For n=1 one has r=0, so the empty product is 1.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[L1]

If G is finite abelian and ∣G∣=∏i<rpiai is its prime factorisation, then the subgroups G(pi) form an internal direct product of G. Thus G≅∏i<rG(pi). For the trivial group, this is the empty product. (A finite abelian group is the internal direct product of its primary components).

[L2]

For a prime p and n>0, isomorphism classes of abelian groups of order pn are in bijection with partitions of n. For n=0, the unique group is the trivial group and corresponds separately to the empty partition. (Isomorphism classes of abelian groups of order p^n are counted by partitions of n).

[L3]

Powers are the natural powers of def-group-power and finite products those of def-monoid-finite-product, both taken in the commutative monoid (Z,⋅,1) of lem-units-of-z. Call p:r→Z an injective list of primes when every pi is prime (def-prime) and pi=pj forces i=j (def-injection-surjection-bijection). Let n∈Z with n≥1 and let p:r→Z be an injective list of primes such that every prime divisor of n equals pi for some i<r. Then, with vq as in def-p-adic-valuation: 1. n  =  ∏i<rpi vpi(n); 2. vq(n)=0 for every prime q that is not among p0,…,pr−1; 3. the exponents are determined by n: if e:r→N and n=∏i<rpi ei, then ej=vpj(n) for every j<r. Clause 3 needs only injectivity of the list, not the covering hypothesis. (For n≥1 and any injective list p:r→Z of primes containing every prime divisor of n, one has n=∏i<rpi vpi(n); the exponents are determined by n, and vq(n)=0 for every prime q outside the list).

[L4]

Let (M,⋅,e) be a monoid (def-semigroup-and-monoid) and let g:N→M be a family of elements of M, written gi:=g(i). There is exactly one function Pg:N→M satisfying Pg(0)=e,Pg(σ(n))=Pg(n)⋅gn(n∈N), and we write ∏i<ngi  :=  Pg(n),also written g0g1⋯gn−1. In particular the empty product is ∏i<0gi=e, and ∏i<1gi=e⋅g0=g0. Why the recursion is legitimate. The clause Pg(σ(n))=Pg(n)⋅gn consults n as well as Pg(n), so thm-recursion does not apply to it directly. Apply that theorem instead with the set A=N×M, the element a=(0,e), and the function F:A→A given by F(n,x)=(σ(n), x⋅gn): it yields a unique H:N→N×M with H(0)=(0,e) and H(σ(n))=F(H(n)). Writing H(n)=(H1(n),H2(n)), induction (thm-induction-principle) gives H1(n)=n for every n, since H1(0)=0 and H1(σ(n))=σ(H1(n)). Hence H(σ(n))=(σ(n), H2(n)⋅gn), so Pg:=H2 satisfies the two displayed equations. It is the only such function: if Q satisfies them too, then {n:Pg(n)=Q(n)} contains 0 and is closed under σ, hence is all of N by induction. The value depends only on g0,…,gn−1. If g,g′:N→M satisfy gi=gi′ for every i<n, then Pg(n)=Pg′(n). Indeed the set of n for which this implication holds contains 0, both products then being e; and if it holds at n, and g,g′ agree at every i<σ(n), then they agree at every i<n and also at n itself, because i<σ(n) is equivalent to i≤n (lem-nat-order-is-membership), so Pg(σ(n))=Pg(n)⋅gn=Pg′(n)⋅gn′=Pg′(σ(n)). Induction finishes it. This is what makes the notation g0g1⋯gn−1 unambiguous: it names a value determined by the first n terms alone, and a finite list u of length n, that is a function u:n→M on the von Neumann natural n={0,…,n−1} (def-natural-numbers), determines the product ∏i<nui:=Pu~(n) computed from any extension u~:N→M of u. (The product g0g1⋯gn−1 of a finite list in a monoid, by recursion, with the empty product (n=0) equal to the identity).

Proof

technique · direct
1.1

Primary decomposition makes an abelian group of order n the product of one abelian pi-group of order piai for each i<r.

givenL1L2L3L4
2.1

The choices for distinct primes are independent and the preceding corollary counts the ith choice by P(ai), so the product rule gives the formula. The empty prime factorisation of 1 gives one choice.

step 1.1∎

Depends on

Used by

Dependency tree · two levels

39 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