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.

Finite-dimensional complex representations of a finite group are determined up to isomorphism by their characters

Statement

Let $G$ be a finite group and let $V$ and $W$ be finite-dimensional complex representations of $G$ . Then

$V ≅ W ⟺ χ_{V} = χ_{W} .$

Facts & Assumptions

Given: A finite group $G$ and finite-dimensional complex representations $V$ and $W$ of $G$ .

[F1]

Every finite-dimensional representation of a finite group over a field of characteristic not dividing $∣ G ∣$ is completely reducible (If $char k ∤ ∣ G ∣$ , every finite-dimensional representation of $G$ is completely reducible).

[F2]

For irreducible $V_{i}$ , the multiplicity of $V_{i}$ in a completely reduced representation $U$ is $m_{i} (U) = ⟨ χ_{U}, χ_{i} ⟩$ (The multiplicity of an irreducible summand is a character inner product).

[A1]

Equivalent representations have equal characters.

Proof

technique · direct

1.1

By [F1] there are decompositions $V ≅ ⨁_{i} m_{i} V_{i}$ and $W ≅ ⨁_{i} n_{i} V_{i}$ over the irreducible representations $V_{i}$ . By [F2] the multiplicities are $m_{i} = ⟨ χ_{V}, χ_{i} ⟩$ and $n_{i} = ⟨ χ_{W}, χ_{i} ⟩$ .

F1F2given

1.2

Conversely, if $V ≅ W$ via an invertible intertwiner, then [A1] gives $χ_{V} = χ_{W}$ . This proves the reverse implication.

A1given

2.1

Assume $χ_{V} = χ_{W}$ . Then every inner product in step 1.1 agrees, so $m_{i} = n_{i}$ for every $i$ ; the two direct sums are built from the same irreducibles with the same multiplicities, hence $V ≅ W$ . This proves the forward implication.

step 1.1algebra

3.1

Steps 2.1 and 1.2 prove both implications, hence the equivalence.

step 2.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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, Corollary 3.3.3 (standard reference, not scraped)