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 cyclotomic field splits a finite group
Statement
If has exponent and is a characteristic-zero field containing all -th roots of unity, then is a splitting field for . In particular is a splitting field.
Facts & Assumptions
The cited prerequisite is Brauer induction.
In characteristic zero, finite-dimensional representations are completely reducible by If , every finite-dimensional representation of is completely reducible.
Proof
Given: is an irreducible complex representation of .
Brauer induction expresses integrally as inductions of linear characters of elementary subgroups. Every such linear character satisfies , so it takes values in and its induced representation has an -model. Thus is the scalar extension of a virtual -representation.
By [F2], decompose that virtual -representation as with the distinct irreducible -representations. Base change preserves intertwiner spaces, so distinct have disjoint irreducible complex constituents. Each is semisimple, with positive constituent multiplicities. Since their signed sum is the single irreducible basis element , exactly one summand occurs, its coefficient and the multiplicity of are both , and it has no other constituent. Hence for that index. Every irreducible complex representation is therefore defined over , so is a splitting field.
The exponent divides , so contains every -th root of unity. Applying the proved assertion to this field gives the final statement. ∎
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
13 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
- Wen-Wei Li, Yanqi Lake Lectures on Algebra I, Corollary 14.4.2 (Lecture 14.4, PDF pp. 171–172) (standard reference, not scraped)