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.
Statement
Let , put and (Common divisor, and the greatest common divisor , with the convention , Common multiple, and the least common multiple , taken to be when or ), and let be a splitting field of over (Every nonzero polynomial over a field has a splitting field), inside which the cyclotomic extensions for are taken (The cyclotomic extension as a splitting field of ). Then
Facts & Assumptions
Given: Integers with and ; is an ordered field (The rationals form a totally ordered field), so (The characteristic of a ring: the least with when one exists, and otherwise) and divides no positive integer (Divisibility in : when for some integer ); a splitting field of over ; and, for each positive divisor of , the subfield of . Write .
For a positive divisor of , the subfield generated by the -th roots of unity in is a cyclotomic extension of of order (The cyclotomic extension as a splitting field of , The group of -th roots of unity in a field, and primitive -th roots of unity); because divides no positive integer, is separable over exactly when the characteristic does not divide , and then a splitting field carries distinct -th roots of unity gives cyclic of order , with exactly primitive -th roots of unity.
for every ( and , The unit group and Euler's totient for , The degree of a finite field extension).
is finite Galois ( is Galois and embeds its Galois group into ).
For finite Galois and finite inside a common field, (For finite Galois and finite inside a common field, ).
For fields with and finite, (Tower law for finite extensions: ).
Proof
divides and , and all divide . For each positive divisor of , write ; then , so splits over the splitting field of , and [L1] applies to . In particular all four cyclotomic extensions for sit inside .
For the inclusion : since , every with satisfies , so and hence ; the same argument with gives .
By [L3] the extension is finite Galois and is finite, both inside , so [L4] and [L5] give , using [L2] twice.
Hence by [L6].
By step 2.1 the tower is defined, and [L7] with [L2] gives , so and .
Remarks
-
Where the base field is used. Only through [L2]: the equality for every , which is irreducibility of over . Over a base field where some becomes reducible the degrees drop unevenly and the degree count in step 2.2 no longer forces the intersection down to .
-
The base field really matters. Over a general base field the same formula can fail; the companion page gives a finite-field witness in is larger than although five and seven are coprime ↗.
Depends on
- $[\mathbb Q(\zeta_n):\mathbb Q]=\varphi(n)$ and $\operatorname{Gal}(\mathbb Q(\mu_n)/\mathbb Q)\cong(\mathbb Z/n)^\times$
- For $E/F$ finite Galois and $L/F$ finite inside a common field, $[EL:F]=[E:F][L:F]/[E\cap L:F]$
- $K(\mu_m)K(\mu_n)=K(\mu_{\operatorname{lcm}(m,n)})$
- $\varphi(m)\varphi(n)=\varphi(\gcd(m,n))\,\varphi(\operatorname{lcm}(m,n))$
- $K(\mu_n)/K$ is Galois and $\sigma\mapsto a_\sigma$ embeds its Galois group into $(\mathbb Z/n)^\times$
- Tower law for finite extensions: $[L:F]=[L:K][K:F]$
- $t^{n}-1$ is separable over $K$ exactly when the characteristic does not divide $n$, and then a splitting field carries $n$ distinct $n$-th roots of unity
- Every nonzero polynomial over a field has a splitting field
- The cyclotomic extension $K(\mu_n)$ as a splitting field of $t^{n}-1$
- The group $\mu_n(K)$ of $n$-th roots of unity in a field, and primitive $n$-th roots of unity
- The degree $[K:F]=\dim_F K$ of a finite field extension
- Common divisor, and the greatest common divisor $\gcd(a,b)$, with the convention $\gcd(0,0) := 0$
- Common multiple, and the least common multiple $\operatorname{lcm}(a,b)$, taken to be $0$ when $a = 0$ or $b = 0$
- The unit group $(\mathbb{Z}/n)^\times$ and Euler's totient $\varphi(n)=\lvert(\mathbb{Z}/n)^\times\rvert$ for $n\ge1$
- The rationals form a totally ordered field
- The characteristic of a ring: the least $n \ge 1$ with $n \cdot 1_R = 0$ when one exists, and $0$ otherwise
- Divisibility in $\mathbb{Z}$: $d \mid a$ when $a = dq$ for some integer $q$
Used by
Dependency tree · two levels
91 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
- K. Conrad, Cyclotomic Extensions (expository blurb), Theorem 3.4 (standard reference, not scraped)
- P. L. Clark, Field Theory (course notes/monograph), Exercise 9.10 (standard reference, not scraped)