Alphabeta Math
TheoremStatement: 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.

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,…,χr of degrees ni=χ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 ∑ini2=∣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.1F1F2given

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.

1.2F4given

Conversely, assume every irreducible character has degree 1, so ni=1 for all i. By [F4], ∣G∣=∑ini2=r.

1.3F5given

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

2.1F3A1step 1.1given

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.

2.2A2step 1.2step 1.3

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.

3.1step 2.1step 2.2∎

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

Depends on

Used by

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