TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

$K (μ_{n}) / K$ is Galois and $σ \mapsto a_{σ}$ embeds its Galois group into $(Z / n)^{\times}$

Statement

Let $K$ be a field and $n \geq 1$ with $char K ∤ n$ (The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise), and let $E = K (μ_{n})$ (The cyclotomic extension $K (μ_{n})$ as a splitting field of $t^{n} - 1$ ). Then $E / K$ is a finite Galois extension, and there is an injective group homomorphism

$Gal (E / K) ⟶ (Z / n)^{\times}, σ ⟼ [a_{σ}]_{n},$

where $a_{σ}$ is any integer with $σ (ζ) = ζ^{a_{σ}}$ for a primitive $n$ -th root of unity $ζ \in E$ . The class $[a_{σ}]_{n}$ does not depend on which primitive $n$ -th root of unity is used, and $σ (x) = x^{a_{σ}}$ holds for every $x \in μ_{n} (E)$ .

Facts & Assumptions

Given: A field $K$ , an integer $n \geq 1$ with $char K ∤ n$ , the extension $E = K (μ_{n})$ (The cyclotomic extension $K (μ_{n})$ as a splitting field of $t^{n} - 1$ ), and a primitive $n$ -th root of unity $ζ \in E$ (The group $μ_{n} (K)$ of $n$ -th roots of unity in a field, and primitive $n$ -th roots of unity).

[L1]

For $n \geq 1$ , $t^{n} - 1$ is separable over $K$ when $char K ∤ n$ ; in a splitting field $E$ the group $μ_{n} (E)$ is then cyclic of order $n$ , has $φ (n)$ primitive $n$ -th roots of unity, and $E = K (ζ)$ for every primitive $n$ -th root of unity $ζ \in E$ ( $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).

[L2]

For a finite extension $L / F$ with $G = Aut (L / F)$ , the conditions " $L / F$ is Galois", " $L$ is the splitting field over $F$ of a separable polynomial", " $∣ G ∣ = [L : F]$ " and " $L^{G} = F$ " are equivalent (Equivalent characterizations of a finite Galois extension, Finite Galois extensions and $Gal (K / F)$ , Relative field automorphisms and $Aut (K / F)$ ).

[L3]

$μ_{n} (E)$ is a finite cyclic subgroup of $E^{\times}$ of order dividing $n$ , and when its order is $n$ its generators are exactly the primitive $n$ -th roots of unity ( $μ_{n} (K)$ is cyclic of order dividing $n$ , and has a primitive $n$ -th root of unity exactly when its order is $n$ ).

[L4]

In a cyclic group $⟨ g ⟩$ of finite order $m$ , $g^{a}$ generates the group if and only if $\gcd (a, m) = 1$ (A cyclic group of order $n$ has exactly $φ (n)$ generators).

[L5]

For an element $x$ of finite order $m$ : $x^{k} = e$ if and only if $m ∣ k$ (If $ord (g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$ , the powers $g^{0}, \dots, g^{n - 1}$ are distinct, and $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ).

[L6]

For $n \geq 1$ and $a \in Z$ , the class $[a]_{n} \in Z / n$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ ) is a unit of $Z / n$ if and only if $\gcd (a, n) = 1$ (For $n \geq 1$ , $[a]_{n}$ is a unit if and only if $\gcd (a, n) = 1$ ); the units form the group $(Z / n)^{\times}$ of order $φ (n)$ (The unit group $(Z / n)^{\times}$ and Euler's totient $φ (n) = ∣ (Z / n)^{\times} ∣$ for $n \geq 1$ ).

[L7]

If $a$ is algebraic over a field $K$ , then the simple extension $K (a) / K$ is finite, with degree equal to the degree of the minimal polynomial of $a$ (A simple algebraic extension is its minimal-polynomial quotient and has power basis $1, a, \dots, a^{n - 1}$ and degree $n$ ).

Proof

technique · direct

1.1L1L2L3L7given

By [L1] the polynomial $t^{n} - 1$ is separable over $K$ , the group $μ_{n} (E)$ is cyclic of order $n$ generated by $ζ$ , and $E = K (ζ)$ . The element $ζ$ is algebraic because it is a root of $t^{n} - 1$ , so [L7] makes $E / K$ finite. Since $E$ is the splitting field of the separable polynomial $t^{n} - 1$ , [L2] now makes $E / K$ finite Galois.

2.1step 1.1given

Each $σ \in Gal (E / K)$ maps $μ_{n} (E)$ into itself, since $σ (x)^{n} = σ (x^{n}) = σ (1) = 1$ ; being injective on the finite set $μ_{n} (E)$ it restricts to a bijection, and it is multiplicative, so it restricts to a group automorphism of $μ_{n} (E)$ .

3.1step 1.1step 2.1L4L5L6

Hence $σ (ζ)$ generates $μ_{n} (E) = ⟨ ζ ⟩$ , so $σ (ζ) = ζ^{a}$ for some integer $a$ , and [L4] gives $\gcd (a, n) = 1$ , so $[a]_{n} \in (Z / n)^{\times}$ by [L6]. The class is well defined: $ζ^{a} = ζ^{b}$ means $ζ^{a - b} = 1$ , which by [L5] and $ord (ζ) = n$ says $n ∣ a - b$ , that is $[a]_{n} = [b]_{n}$ . Write $[a_{σ}]_{n}$ for this class.

4.1step 1.1step 3.1

For every $x \in μ_{n} (E)$ one has $x = ζ^{j}$ for some $j$ , so $σ (x) = σ (ζ)^{j} = ζ^{a_{σ} j} = x^{a_{σ}}$ .

4.2step 3.1L6

The map $σ \mapsto [a_{σ}]_{n}$ is a group homomorphism: $(σ τ) (ζ) = σ (ζ^{a_{τ}}) = σ (ζ)^{a_{τ}} = ζ^{a_{σ} a_{τ}}$ , so $[a_{σ τ}]_{n} = [a_{σ}]_{n} [a_{τ}]_{n}$ by the well-definedness of step 3.1.

4.3step 1.1step 3.1

It is injective: if $[a_{σ}]_{n} = [1]_{n}$ then $σ (ζ) = ζ$ by step 3.1, and since $E = K (ζ)$ and $σ$ fixes $K$ pointwise, $σ$ is the identity on $E$ .

5.1step 1.1step 3.1step 4.1step 4.2step 4.3L3∎

The class is independent of the chosen primitive $n$ -th root of unity: any other one is a generator $ζ^{'}$ of $μ_{n} (E)$ by [L3], so $ζ^{'} = ζ^{b}$ for some $b$ , and $σ (ζ^{'}) = σ (ζ)^{b} = ζ^{a_{σ} b} = (ζ^{b})^{a_{σ}} = (ζ^{'})^{a_{σ}}$ , which exhibits the same exponent class. With steps 4.1, 4.2 and 4.3 this proves the theorem.

Remarks

The embedding need not be onto. Surjectivity is exactly irreducibility of the $n$ -th cyclotomic polynomial over $K$ ( $Φ_{n}$ is irreducible over $K$ exactly when $[K (ζ_{n}) : K] = φ (n)$ , exactly when the embedding into $(Z / n)^{\times}$ is onto), and it fails over many base fields: over $F_{q}$ the image is the cyclic subgroup generated by the class of $q$ (For $\gcd (n, q) = 1$ the image of $Gal (F_{q} (μ_{n}) / F_{q})$ in $(Z / n)^{\times}$ is generated by $[q]$ ).

Depends on

Used by

Dependency tree · two levels

89 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), Lemma 2.1 and Theorem 2.3 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, Proposition 5.8 (standard reference, not scraped)
P. L. Clark, Field Theory (course notes/monograph), Proposition 9.5 (standard reference, not scraped)

K(μn)/KK(μn​)/K is Galois and σ↦aσσ↦aσ​ embeds its Galois group into (Z/n)×(Z/n)×