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

The multiplicity of an irreducible summand is a character inner product

Statement

Let $G$ be a finite group, let $V$ be a finite-dimensional complex representation of $G$ . Choose representatives $V_{1}, \dots, V_{r}$ of the irreducible representations, write $χ_{j} : = χ_{V_{j}}$ , and write $V ≅ ⨁_{j = 1}^{r} m_{j} V_{j}$ . Then the multiplicity of $V_{i}$ in $V$ is

$m_{i} = ⟨ χ_{V}, χ_{i} ⟩ .$

Facts & Assumptions

Given: A finite group $G$ , a finite-dimensional complex representation $V$ of $G$ , representatives $V_{j}$ of the irreducible representations with characters $χ_{j} : = χ_{V_{j}}$ , a decomposition $V ≅ ⨁_{j} m_{j} V_{j}$ , and an index $i$ .

[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]

Characters add on direct sums (Characters add on direct sums, multiply on tensor products, and conjugate on duals).

[F3]

Irreducible characters are orthonormal: $⟨ χ_{j}, χ_{i} ⟩ = δ_{j i}$ (The first orthogonality relation for irreducible complex characters).

Proof

technique · direct

1.1

Since $char C = 0$ does not divide $∣ G ∣$ , [F1] gives a decomposition $V ≅ ⨁_{j} m_{j} V_{j}$ with each $V_{j}$ irreducible.

F1given

2.1

Applying [F2] iteratively to the decomposition of step 1.1 gives $χ_{V} = \sum_{j} m_{j} χ_{j}$ , a finite sum because $V$ is finite-dimensional.

F2step 1.1

3.1

Taking the inner product with $χ_{i}$ , linearity in the first argument and [F3] give $⟨ χ_{V}, χ_{i} ⟩ = \sum_{j} m_{j} ⟨ χ_{j}, χ_{i} ⟩ = \sum_{j} m_{j} δ_{j i} = m_{i}$ .

F3step 2.1algebra∎

Depends on

Used by

Dependency tree · two levels

16 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.1 (standard reference, not scraped)