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.
Dual group of a finite abelian group
Definition
Let be a finite abelian group (Group and abelian group) written additively. Its set of additive characters is where an additive character is the group homomorphism of Additive characters of a finite abelian group. For , define their pointwise product by . The constant-one function is denoted , and the pointwise inverse is .
This specifies a set and operations. The later theorem thm-qa-finite-abelian-character-dual-is-finite-abelian-group proves that these operations make a finite abelian group; no isomorphism is part of this definition.
Depends on
Used by
- Character annihilator of a subgroup Definition
- Finite abelian hidden-subgroup promise and output encoding Definition
- Normalized Fourier transform on a finite abelian group Definition
- Finite abelian Fourier and convolution examples Example
- A cyclic group of order n has exactly n additive characters Lemma
- Characters of a finite product factor coordinatewise Lemma
- Fourier annihilator equation for cyclic discrete logarithm Lemma
- A finite abelian group and its character dual have equal order Theorem
- Dual-index character orthogonality Theorem
- Finite abelian group is canonically isomorphic to its double dual Theorem
- Pointwise character dual is a finite abelian group Theorem
Dependency tree · two levels
13 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)