TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

A finite group is abelian if and only if all its irreducible complex characters have degree $1$

Statement

Let $G$ be a finite group. Then $G$ is abelian if and only if every irreducible complex character of $G$ has degree $1$ .

Facts & Assumptions

Given: A finite group $G$ with irreducible characters $χ_{1}, \dots, χ_{r}$ of degrees $n_{i} = χ_{i} (1)$ .

[F1]

Over an algebraically closed field, every intertwiner from an irreducible representation to itself is a scalar (Over an algebraically closed field, every endomorphism of an irreducible representation is scalar).

[F2]

A field $k$ is a splitting field for $G$ when every irreducible representation $V$ has ${End}_{G} (V) = k$ (A splitting field for a finite group: every irreducible representation has scalar endomorphism ring).

[F3]

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).

[F4]

The degrees of the irreducible characters satisfy $\sum_{i} n_{i}^{2} = ∣ G ∣$ (The regular character gives a second proof of the sum-of-squares formula).

[F5]

The number of irreducible representations of $G$ up to equivalence equals the number of conjugacy classes, when the field is algebraically closed of characteristic not dividing $∣ G ∣$ (If $k$ is algebraically closed and $char k ∤ ∣ G ∣$ , the number of irreducible representations of $G$ equals the number of conjugacy classes).

[A1]

The degree of an irreducible character is the dimension of any representation affording it.

[A2]

A finite group is abelian exactly when every conjugacy class has one element.

Proof

technique · direct

1.1

Assume $G$ is abelian. For every irreducible representation $V$ of $G$ , [F1] gives ${End}_{G} (V) = C$ ; by [F2], $C$ is a splitting field for $G$ .

F1F2given

1.2

Conversely, assume every irreducible character has degree $1$ , so $n_{i} = 1$ for all $i$ . By [F4], $∣ G ∣ = \sum_{i} n_{i}^{2} = r$ .

F4given

1.3

Since $C$ is algebraically closed and $char C = 0$ does not divide $∣ G ∣$ , [F5] applies: $r$ equals the number of conjugacy classes of $G$ .

F5given

2.1

By [F3] applied over this splitting field, every irreducible representation of the abelian group $G$ has degree $1$ ; by [A1] every irreducible character has degree $1$ . This proves the forward implication.

F3A1step 1.1given

2.2

Steps 1.2 and 1.3 show $∣ G ∣$ equals the number of conjugacy classes, so the $∣ G ∣$ conjugacy classes each have exactly one element; by [A2], $G$ is abelian. This proves the reverse implication.

A2step 1.2step 1.3

3.1

Steps 2.1 and 2.2 prove the two implications, hence the equivalence.

step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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, Theorem 4.1.5 (standard reference, not scraped)

A finite group is abelian if and only if all its irreducible complex characters have degree 11