ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29

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 irreducible complex characters of a finite cyclic group are the $n$ powers of a primitive $n$ th root

Example

Let $G = ⟨ g ⟩$ be a cyclic group of order $n \geq 1$ , and let $ζ \in C$ be a primitive $n$ -th root of unity. The irreducible complex characters of $G$ are exactly

$χ_{k} (g^{m}) : = ζ^{k m} (0 \leq k \leq n - 1),$

and they are pairwise distinct.

Facts & Assumptions

Given: A cyclic group $G = ⟨ g ⟩$ of order $n \geq 1$ .

[F1]

A cyclic group of order $n$ is isomorphic to $Z / n$ (Every cyclic group is isomorphic to $(Z, +)$ or to $(Z / n, +)$ for its finite order $n \geq 1$ ).

[F2]

Choosing a basis identifies degree-one representations with homomorphisms $G \to C^{\times}$ , and two such representations are equivalent exactly when the homomorphisms agree (Equivalence classes of degree-one representations are exactly homomorphisms $G \to k^{\times}$ ; equivalently they factor through $G / G^{'}$ , and they form an abelian group).

[F3]

The roots of $x^{n} - 1$ in a field form a finite cyclic subgroup $μ_{n}$ whose order divides $n$ . This group contains a primitive $n$ -th root exactly when it has order $n$ , and in that case its generators are exactly the primitive $n$ -th roots. ( $μ_{n} (K)$ is cyclic of order dividing $n$ , and has a primitive $n$ -th root of unity exactly when its order is $n$ )

[F4]

Over a field of characteristic not dividing $n$ , a splitting field of $t^{n} - 1$ has exactly $n$ distinct $n$ -th roots of unity, and they form a cyclic group of order exactly $n$ ( $t^{n} - 1$ is separable over $K$ exactly when the characteristic does not divide $n$ , and then a splitting field carries $n$ distinct $n$ -th roots of unity).

[F5]

Over an algebraically closed field, every endomorphism of an irreducible representation is scalar (Over an algebraically closed field, every endomorphism of an irreducible representation is scalar).

[F6]

A field is a splitting field for a finite group exactly when every irreducible representation has scalar endomorphism ring (A splitting field for a finite group: every irreducible representation has scalar endomorphism ring).

[F7]

Every irreducible representation of a finite abelian group over a splitting field has degree $1$ (Every irreducible representation of a finite abelian group over a splitting field is one-dimensional).

Verification

technique · direct

1.1F3F4given

Since $g^{n} = 1$ , a homomorphism $φ : G \to C^{\times}$ sends $g$ to an $n$ -th root of unity: $φ (g)^{n} = φ (g^{n}) = φ (1) = 1$ . By [F4] the $n$ -th roots of unity in $C$ are exactly the $n$ distinct powers $ζ^{0}, \dots, ζ^{n - 1}$ of a primitive root $ζ$ of [F3].

1.2F1F3givenalgebra

For each $k$ , the formula $χ_{k} (g^{m}) = ζ^{k m}$ is well defined by [F1] and is a homomorphism, since $χ_{k} (g^{a} g^{b}) = ζ^{k (a + b)} = ζ^{k a} ζ^{k b}$ . They are pairwise distinct because $ζ^{k - k^{'}} \neq 1$ for $0 < ∣ k - k^{'} ∣ < n$ by primitivity of [F3].

2.1F2F5F6F7step 1.1step 1.2∎

By [F5] and [F6], $C$ is a splitting field for the finite abelian group $G$ ; then [F7] shows every irreducible representation of $G$ has degree $1$ . By [F2] it corresponds to a homomorphism $φ : G \to C^{\times}$ , and step 1.1 shows $φ (g) = ζ^{k}$ for some $k$ , so $φ = χ_{k}$ . Hence the irreducible characters are exactly the $χ_{k}$ .

Depends on

Used by

The character table of a finite cyclic group over ℂ Example

Dependency tree · two levels

47 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

Pavel Etingof et al., Introduction to Representation Theory, Section 3.3 (standard reference, not scraped)
Peter Webb, A Course in Finite Group Representation Theory, Section 4.1 (standard reference, not scraped)

The irreducible complex characters of a finite cyclic group are the nn powers of a primitive nnth root