TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

For $\gcd (n, q) = 1$ the image of $Gal (F_{q} (μ_{n}) / F_{q})$ in $(Z / n)^{\times}$ is generated by $[q]$

Statement

Let $F_{q}$ be a finite field of order $q$ (Finite fields and their order) and let $n \geq 1$ with $\gcd (n, q) = 1$ (Coprime integers: $\gcd (a, b) = 1$ ). Then the image of the embedding

$Gal (F_{q} (μ_{n}) / F_{q}) ⟶ (Z / n)^{\times}$

of $K (μ_{n}) / K$ is Galois and $σ \mapsto a_{σ}$ embeds its Galois group into $(Z / n)^{\times}$ is the cyclic subgroup generated by $[q]_{n}$ , and

$[F_{q} (μ_{n}) : F_{q}] = ord ([q]_{n}),$

the multiplicative order of $[q]_{n}$ in $(Z / n)^{\times}$ (The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity).

Facts & Assumptions

Given: A finite field $F_{q}$ of order $q$ , of characteristic $p$ with $q$ a power of $p$ (Every finite field has order $p^{n}$ for a unique prime characteristic $p$ and positive integer $n$ ), and an integer $n \geq 1$ with $\gcd (n, q) = 1$ ; the extension $E : = F_{q} (μ_{n})$ (The cyclotomic extension $K (μ_{n})$ as a splitting field of $t^{n} - 1$ ).

[L1]

For a field $K$ and $n \geq 1$ with $char K ∤ n$ , the extension $K (μ_{n}) / K$ is finite Galois and $σ \mapsto [a_{σ}]_{n}$ , determined by $σ (ζ) = ζ^{a_{σ}}$ on a primitive $n$ -th root of unity, is an injective homomorphism into $(Z / n)^{\times}$ with $σ (x) = x^{a_{σ}}$ for every $x \in μ_{n}$ ( $K (μ_{n}) / K$ is Galois and $σ \mapsto a_{σ}$ embeds its Galois group into $(Z / n)^{\times}$ ).

[L2]

An extension $L / F_{q}$ of finite fields of degree $m$ is Galois with $Gal (L / F_{q}) = ⟨ σ_{q} ⟩$ cyclic of order $m$ , where $σ_{q} (x) = x^{q}$ (A finite extension of a finite field of order $q$ is Galois with cyclic Galois group generated by $x \mapsto x^{q}$ , The relative Frobenius $x \mapsto x^{q}$ of an extension of finite fields).

[L3]

For $n \geq 1$ and $a \in Z$ , the class $[a]_{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 unit group $(Z / n)^{\times}$ and Euler's totient $φ (n) = ∣ (Z / n)^{\times} ∣$ for $n \geq 1$ ).

[L4]

For a finite Galois extension $L / F$ one has $∣ Gal (L / F) ∣ = [L : F]$ (Equivalent characterizations of a finite Galois extension, The degree $[K : F] = \dim_{F} K$ of a finite field extension).

Proof

technique · direct

1.1

The characteristic $p$ divides $q$ , and $\gcd (n, q) = 1$ , so $p ∤ n$ ; hence [L1] applies to $K = F_{q}$ and $E = F_{q} (μ_{n})$ is finite Galois over $F_{q}$ . Also $[q]_{n}$ is a unit of $Z / n$ by [L3].

L1L3given

2.1

$E$ is a finite field: it is a finite extension of the finite field $F_{q}$ by step 1.1, so it is a finite-dimensional $F_{q}$ -vector space over a finite field and therefore has finitely many elements. By [L2], $Gal (E / F_{q}) = ⟨ σ_{q} ⟩$ with $σ_{q} (x) = x^{q}$ .

step 1.1L2

3.1

The exponent attached to $σ_{q}$ by [L1] is $[q]_{n}$ , since $σ_{q} (ζ) = ζ^{q}$ for a primitive $n$ -th root of unity $ζ \in E$ . Because the embedding is a homomorphism and $Gal (E / F_{q})$ is generated by $σ_{q}$ , the image is the subgroup of $(Z / n)^{\times}$ generated by $[q]_{n}$ .

step 1.1step 2.1L1

4.1

The embedding is injective, so $∣ Gal (E / F_{q}) ∣$ equals the order of $⟨ [q]_{n} ⟩$ , which is $ord ([q]_{n})$ ; and $[E : F_{q}] = ∣ Gal (E / F_{q}) ∣$ by [L4]. Hence $[E : F_{q}] = ord ([q]_{n})$ .

step 3.1L1L4∎

Remarks

What the coprimality hypothesis does. It makes $[q]_{n}$ a unit, so that the subgroup it generates is defined, and it puts the extension inside the scope of [L1] by ruling out $char F_{q} ∣ n$ . Without it the group $μ_{n}$ collapses onto $μ_{m}$ for the prime-to- $p$ part $m$ of $n$ (In characteristic $p$ the only $p^{k}$ -th root of unity is $1$ , and $t^{p^{k}} - 1 = (t - 1)^{p^{k}}$ ), and the statement is about $m$ rather than $n$ .

Depends on

Used by

Dependency tree · two levels

71 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 2.10 (standard reference, not scraped)
K. Conrad, Finite Fields (expository blurb), Theorem 5.6 (standard reference, not scraped)

For gcd⁡(n,q)=1gcd(n,q)=1 the image of Gal⁡(Fq(μn)/Fq)Gal(Fq​(μn​)/Fq​) in (Z/n)×(Z/n)× is generated by [q][q]