Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-29
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.

Minimal polynomials of integral elements over an integrally closed domain have coefficients in the domain

Statement

Let A be an integrally closed domain with field of fractions K, let L/K be a field extension, and let uL be integral over A. Then the minimal polynomial of u over K has coefficients in A.

In particular, if f(T)A[T] is monic and factors in K[T] as

f(T)=(Ta)h(T)

with aK, then h(T)A[T].

Facts & Assumptions

Given: An integrally closed domain A with field of fractions K, a field extension L/K, and an element uL integral over A.

[L1]

The phrase "integrally closed domain" means that every element of K integral over A already lies in A (Integral closure in an extension ring and integrally closed domains).

[L2]

Integral elements over a nonzero base ring form a subring (Integral elements over a nonzero base ring form a subring).

[L3]

An algebraic element over a field has a unique monic irreducible minimal polynomial, and it divides every polynomial that vanishes at that element (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

[L4]

Every nonzero polynomial over a field has a splitting field (Every nonzero polynomial over a field has a splitting field).

[L5]

If a monic irreducible polynomial over a field has two roots in extensions, there is a field homomorphism between the simple extensions sending one root to the other (Universal property of adjoining a root of an irreducible polynomial).

Proof

technique · direct
1.1

By [L3], the minimal polynomial mu(T)K[T] of u is monic and irreducible. Since u is integral over A, it satisfies some monic polynomial in A[T], so [L3] implies that mu is nonzero. By [L4], choose a splitting field E/K for mu and write mu(T)=i=1n(Tαi) with α1=u.

L3L4given
2.1

Let g(T)A[T] be a monic polynomial with g(u)=0. For each root αi of mu, the universal property [L5] gives a K-homomorphism K[u]E sending u to αi. Applying that homomorphism to the identity g(u)=0 shows g(αi)=0. Thus every αi is integral over A.

L1L5step 1.1given
3.1

The coefficients of mu are, up to sign, the elementary symmetric polynomials in the integral elements α1,,αn. Since A is a domain and therefore nonzero, [L2] shows that these symmetric polynomials are integral over A. But the coefficients also lie in K, so [L1] forces them to lie in A. This proves the first statement.

L1L2step 2.1algebra
4.1

For the factor statement, choose a splitting field of f over K and write f(T)=(Ta)i=2n(Tβi). Each βi is integral over A because it is a root of the monic polynomial fA[T]. Therefore the coefficients of h(T)=i=2n(Tβi) are integral over A by the same symmetric-polynomial argument as in step 3.1, and they lie in K because hK[T]. Hence [L1] forces all coefficients of h to lie in A.

L1L2L4step 3.1algebra

Depends on

Used by

Dependency tree · two levels

18 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