TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

A finite abelian group and its character dual have equal order

Statement

If $G$ is a finite abelian group with invariant-factor decomposition $G ≅ C_{n_{1}} \times \dots \times C_{n_{r}}$ , then $∣ \hat{G} ∣ = \prod_{i} n_{i} = ∣ G ∣$ . The empty product is allowed: it represents the trivial group and has value $1$ . This is a finite-set cardinality assertion; it does not choose an isomorphism $G ≅ \hat{G}$ .

Facts & Assumptions

Given: A finite abelian group $G$ .

[F1]

Every finite abelian group has an invariant-factor decomposition; the trivial group corresponds to the empty list (Fundamental theorem of finite abelian groups: invariant-factor form).

[F2]

Characters of a finite direct product factor coordinatewise (Characters of a finite product factor coordinatewise).

[F3]

A cyclic group of order $n \geq 1$ has exactly $n$ characters, including the case $n = 1$ (A cyclic group of order n has exactly n additive characters).

[F4]

A binary external direct product of finite groups has order the product of the two orders (For finite groups $G$ and $H$ , $∣ G \times H ∣ = ∣ G ∣ ∣ H ∣$ ).

[F5]

A Cartesian product of finite sets has cardinality the product of the cardinalities (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ).

[F6]

A group isomorphism is a bijective group homomorphism (Group isomorphisms, automorphisms and the set $Aut (G)$ ); the order of a finite group is the cardinality of its carrier (The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity).

[F7]

The inverse of a bijective group homomorphism is a group homomorphism (The inverse of a bijective group homomorphism is a group homomorphism).

[F8]

$\hat{G}$ denotes the set of additive characters with its specified pointwise operations (Dual group of a finite abelian group).

Proof

1.1F1F3F8

If the invariant-factor list is empty, [F1] identifies $G$ with the trivial group, which is cyclic of order $1$ . By [F3] it has one character and one element, so $∣ \hat{G} ∣ = ∣ G ∣ = 1$ for the character set in [F8].

1.2F1F6F7F8construct

Otherwise fix one isomorphism $φ : G \to P$ , where $P = C_{n_{1}} \times \dots \times C_{n_{r}}$ is the finite iterated product. By [F6] and [F7], both $φ$ and $φ^{- 1}$ are group homomorphisms. Thus $χ \mapsto χ \circ φ^{- 1}$ and $ψ \mapsto ψ \circ φ$ preserve the character sets in [F8] and are inverse bijections between $\hat{G}$ and $\hat{P}$ .

1.3F2F3F5

By [F2], $\hat{P}$ is in bijection with $\prod_{i} \hat{C_{n_{i}}}$ . Each factor has $n_{i}$ elements by [F3], and repeated application of [F5] to the finite Cartesian products gives $∣ \hat{P} ∣ = \prod_{i} n_{i}$ .

2.1step 1.2step 1.3F4F6∎

The same repeated product-order formula gives $∣ P ∣ = \prod_{i} n_{i}$ by [F4]; the isomorphism in step 1.2 preserves finite cardinality by [F6]. Hence $∣ G ∣ = \prod_{i} n_{i} = ∣ \hat{G} ∣$ .

Depends on

Used by

Normalized Fourier transform on a finite abelian group Definition
Dual-index character orthogonality Theorem
Finite abelian Fourier transform is unitary Theorem
Finite abelian group is canonically isomorphic to its double dual Theorem
Pointwise character dual is a finite abelian group Theorem
Subgroup-annihilator cardinality Theorem

Dependency tree · two levels

38 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

Ronald de Wolf, Quantum Computing: Lecture Notes, version 6 (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms (standard reference, not scraped)
John Preskill, Quantum Information, Chapter 6: Quantum Algorithms (standard reference, not scraped)