CorollaryStatement: Literature-sourcedProof: 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.

For $g \in G$ , the sum of $∣ χ_{i} (g) ∣^{2}$ over the irreducible complex characters is $∣ C_{G} (g) ∣$

Statement

Let $G$ be a finite group with irreducible complex characters $χ_{1}, \dots, χ_{r}$ . For every $g \in G$ ,

$\sum_{i = 1}^{r} ∣ χ_{i} (g) ∣^{2} = ∣ C_{G} (g) ∣ .$

Facts & Assumptions

Given: A finite group $G$ , its irreducible characters $χ_{1}, \dots, χ_{r}$ , and an element $g \in G$ .

[F1]

For $g, h \in G$ , $\sum_{i} χ_{i} (g) \overline{χ_{i} (h)} = ∣ C_{G} (g) ∣$ when $h$ is conjugate to $g$ , and $0$ otherwise (The second orthogonality relation for irreducible complex characters).

Proof

technique · direct

1.1F1given

The element $g$ is conjugate to itself, so applying [F1] with $h = g$ gives $\sum_{i} χ_{i} (g) \overline{χ_{i} (g)} = ∣ C_{G} (g) ∣$ .

2.1step 1.1algebra∎

Each summand equals $∣ χ_{i} (g) ∣^{2}$ , so the sum of step 1.1 is exactly $\sum_{i} ∣ χ_{i} (g) ∣^{2}$ , which proves the claim.

Depends on

The second orthogonality relation for irreducible complex characters

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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

Peter Webb, A Course in Finite Group Representation Theory, Section 3.4 (standard reference, not scraped)

For g∈Gg∈G, the sum of ∣χi(g)∣2∣χi​(g)∣2 over the irreducible complex characters is ∣CG(g)∣∣CG​(g)∣