LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

Artin's ideal generated by $f (x_{f})$ for all monic nonconstant $f \in F [x]$ is proper

Statement

Let $S$ be the set of monic nonconstant polynomials in $F [x]$ , let $A = F [x_{f} : f \in S]$ , and let

$I = (f (x_{f}) : f \in S) ⊴ A .$

Then $I$ is a proper ideal of $A$ .

Facts & Assumptions

Given: A field $F$ , the family polynomial ring $A = F [x_{f} : f \in S]$ , and the ideal $I$ displayed in the Statement.

[L1]

The family polynomial ring consists of finite sums involving only finitely many indeterminates (The polynomial ring $R [x_{i} : i \in I]$ as finitely supported coefficient families on monomials).

[L2]

A homomorphism from a family polynomial ring is obtained by assigning an image to every indeterminate, and is unique with those assignments (Universal property of a polynomial ring on an arbitrary family of indeterminates).

[L3]

A finite family of nonzero polynomials has a common splitting field (Every finite family of nonzero polynomials has a splitting field, obtained from their product).

Proof

technique · contradiction

1.1

Suppose $I = A$ . Then $1 = \sum_{j = 1}^{m} h_{j} f_{j} (x_{f_{j}})$ for finitely many $f_{j} \in S$ and $h_{j} \in A$ .

assume-contraL1

1.2

By [L3], choose a field $E / F$ in which all $f_{j}$ split, and choose a root $a_{j} \in E$ of each $f_{j}$ .

L3choose

2.1

Assign $x_{f_{j}} \mapsto a_{j}$ for the variables occurring as generators in step 1.1 and assign every other indeterminate, including unused ones appearing in the $h_{j}$ , to $0$ . By [L2] this gives an $F$ -algebra homomorphism $Φ : A \to E$ .

step 1.1step 1.2L2construct

3.1

Applying $Φ$ to step 1.1 gives $1 = \sum_{j} Φ (h_{j}) f_{j} (a_{j}) = 0$ , impossible in the field $E$ . Therefore $I$ is proper.

step 1.1step 1.2step 2.1discharge-contradiction∎

Depends on

Used by

Assuming Choice, every field has an algebraic extension containing roots of all nonconstant base polynomials Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 41 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. S. Milne, Fields and Galois Theory, Chapter 6 (standard reference, not scraped)
P. L. Clark, Field Theory, Theorem 4.9 (standard reference, not scraped)

Artin's ideal generated by f(xf)f(xf​) for all monic nonconstant f∈F[x]f∈F[x] is proper