LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.1assume-contraL1

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$ .

1.2L3choose

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}$ .

2.1step 1.1step 1.2L2construct

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$ .

3.1step 1.1step 1.2step 2.1discharge-contradiction∎

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.

Depends on

Used by

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

Dependency tree · two levels

13 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

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