LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05

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 generator-indicator class function of a cyclic group is obtained by Mobius inversion

Statement

Let $C$ be a finite cyclic group, and define a class function $η_{C} : C \to Z$ by

$η_{C} (c) = {\begin{cases} ∣ C ∣, & ⟨ c ⟩ = C, \\ 0, & ⟨ c ⟩ \neq C . \end{cases}$

Then

$η_{C} = \sum_{D \leq C} μ (∣ C : D ∣) ∣ D ∣ {Ind}_{D}^{C} 1_{D},$

where $μ$ is the classical number-theoretic Mobius function, characterized by

$\sum_{d ∣ n} μ (d) = {\begin{cases} 1, & n = 1, \\ 0, & n > 1. \end{cases}$

Facts & Assumptions

Given: A finite cyclic group $C$ and an element $c \in C$ .

[F1]

The subgroup $⟨ c ⟩$ generated by $c$ is the smallest subgroup of $C$ containing $c$ (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[F2]

For a subgroup $D \leq C$ , Frobenius' formula gives ${Ind}_{D}^{C} 1_{D} (c) = \frac{1}{∣ D ∣} \sum_{\begin{array}{c} x \in C \\ x^{- 1} c x \in D \end{array}} 1.$ (Frobenius' formula for the character of an induced representation)

[F3]

For every positive integer $n$ , the divisor sum of the classical Mobius function satisfies $\sum_{d ∣ n} μ (d) = {\begin{cases} 1, & n = 1, \\ 0, & n > 1. \end{cases}$

Proof

technique · direct

1.1

Let $E : = ⟨ c ⟩$ . By [F1], for every subgroup $D \leq C$ one has $c \in D$ if and only if $E \leq D$ . Choose a generator $g$ of $C$ . For each divisor $m$ of $∣ C ∣$ , the subgroup $⟨ g^{∣ C ∣ / m} ⟩$ has order $m$ , so cyclic subgroups of $C$ are uniquely indexed by the divisors of $∣ C ∣$ . If $H, K \leq C$ have orders $m, n$ , then $H \leq K$ holds exactly when $m ∣ n$ , because with the displayed indexing one has $⟨ g^{∣ C ∣ / m} ⟩ \leq ⟨ g^{∣ C ∣ / n} ⟩$ exactly when $∣ C ∣ / n$ divides $∣ C ∣ / m$ .

F1givenalgebra

2.1

The quotient $∣ C : E ∣$ is a positive integer. If $E \leq D \leq C$ , then $∣ C : E ∣ = ∣ C : D ∣ ∣ D : E ∣$ , so the index $∣ C : D ∣$ divides $∣ C : E ∣$ . Conversely, if $d$ is a positive divisor of $∣ C : E ∣$ , put $m : = ∣ C ∣ / d$ . Then $∣ E ∣$ divides $m$ , so by step 1.1 the unique subgroup $D \leq C$ of order $m$ contains $E$ and satisfies $∣ C : D ∣ = d$ . Therefore the positive divisors of $∣ C : E ∣$ are exactly the indices $∣ C : D ∣$ for subgroups $D$ with $E \leq D \leq C$ . Hence [F3] gives $\sum_{E \leq D \leq C} μ (∣ C : D ∣) = \sum_{d ∣ ∣ C : E ∣} μ (d) = {\begin{cases} 1, & ∣ C : E ∣ = 1, \\ 0, & ∣ C : E ∣ > 1. \end{cases}$ Since $∣ C : E ∣ = 1$ holds exactly when $E = C$ , this is $1_{{⟨ c ⟩ = C}}$ .

F3step 1.1algebra

3.1

Because $C$ is abelian, $x^{- 1} c x = c$ for every $x \in C$ , so [F2] becomes ${Ind}_{D}^{C} 1_{D} (c) = ∣ C ∣ / ∣ D ∣$ when $c \in D$ and ${Ind}_{D}^{C} 1_{D} (c) = 0$ when $c \notin D$ . Using step 1.1, the right-hand side of the claimed formula evaluates at $c$ to $\sum_{D \leq C} μ (∣ C : D ∣) ∣ D ∣ {Ind}_{D}^{C} 1_{D} (c) = ∣ C ∣ \sum_{E \leq D \leq C} μ (∣ C : D ∣) = ∣ C ∣ 1_{{⟨ c ⟩ = C}}$ , which is exactly $η_{C} (c)$ by step 2.1.

F2step 1.1step 2.1algebra

4.1

The equality of step 3.1 holds for every $c \in C$ , so the two class functions are equal.

step 3.1∎

Depends on

Used by

Dependency tree · two levels

9 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

Janos Kramar, Artin's and Brauer's Theorems on Induced Characters, the definition of chi_H and Lemma 2 (standard reference, not scraped)
Kay Yang, Rational Valued Characters, Lemma 5 (standard reference, not scraped)
Tammo tom Dieck, Representation Theory, Section 4.5 (standard reference, not scraped)