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

If μnF and charFn, then a degree-n extension is cyclic exactly when it is F(α) with αnF and xnαn irreducible

Statement

Let F be a field, let n1, assume charFn, and assume F contains a primitive n-th root of unity. For a finite extension K/F of degree n, the following are equivalent:

  1. K/F is cyclic.
  2. There exists αK such that K=F(α), αnF, and xnαn is irreducible over F.

Facts & Assumptions

Given: A field F, an integer n1, a primitive n-th root of unity ζF, and a finite extension K/F of degree n.

[F1]

The Lagrange resolvent is Rσ,ζ(x)=i=0n1ζiσi(x) (The Lagrange resolvent attached to a cyclic action and a root of unity).

[L1]

Distinct characters are linearly independent (Dedekind's linear independence theorem for distinct characters).

[L2]

If an extension contains one nonzero root α of xna, then all roots are ζiα, and the splitting field is obtained by adjoining α and the relevant roots of unity (After adjoining one nonzero root α of xna, all roots are ζα with ζn=1).

[L3]

When charFn, the polynomial xn1 is separable and a splitting field has cyclic root-of-unity group of order n (tn1 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).

[L4]

A finite extension is Galois exactly when it is the splitting field of a separable polynomial (Equivalent characterizations of a finite Galois extension).

[L5]

Embeddings of a simple algebraic extension correspond to the distinct roots of the minimal polynomial (F-embeddings of F(α) into an algebraically closed field correspond to the distinct roots of mα).

Proof

technique · direct
1.1

For the forward direction, assume K/F is cyclic and choose a generator σ of Gal(K/F). The distinct powers 1,σ,,σn1 are distinct characters K×K×, so [L1] makes the resolvent operator Rσ,ζ of [F1] nonzero. Choose γK with α:=Rσ,ζ(γ)0.

F1L1choose
1.2

For the converse direction, assume K=F(α), αn=aF, and xna is irreducible. If α=0, then a=0 and the irreducible polynomial is xn, which forces n=1. Hence K=F, so the extension is cyclic. Assume from now on that α0. Then [K:F]=n, and [L2] shows every root of xna is ζiα with ζiF. Because [L3] makes the n roots of xn1 distinct, these roots ζiα are distinct as well. Hence all roots of xna already lie in K, and the polynomial is separable, so K is its splitting field and [L4] makes K/F Galois.

L2L3L4algebra
2.1

In the nonzero case of step 1.2, the root ζα of the irreducible polynomial xna determines, by [L5], an F-embedding K=F(α)K sending α to ζα, hence an automorphism τ of K/F. Its powers send α to ζiα, so τ has order n. Because [K:F]=n and a finite Galois extension has at most [K:F] automorphisms, Gal(K/F)=τ is cyclic of order n.

step 1.2L4L5algebra
2.2

Because σ(α)=i=0n1ζiσi+1(γ)=ζα, the element αn is fixed by σ and hence by the whole cyclic Galois group, so αnF. If 0<d<n and αdF, then αd=σ(αd)=ζdαd, so ζd=1, contradicting primitivity of ζ. Therefore no smaller positive power of α lies in F. The minimal polynomial of α divides xnαn and has degree n=[K:F], so it is exactly xnαn and K=F(α).

step 1.1algebra
3.1

Steps 2.2 and 2.1 prove the equivalence.

step 2.2step 2.1

Remarks

  • The irreducibility clause is what forces degree exactly n. Without it, adjoining one n-th root can produce a proper divisor of n.

Depends on

Used by

Dependency tree · two levels

42 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