CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-30

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.

Strong Nullstellensatz: I(V(I)) equals the radical of I

Statement

Assume the Axiom of Choice.

Let $k$ be an algebraically closed field and let $I \subseteq k [x_{1}, \dots, x_{n}]$ be an ideal. Then $I (V (I)) = \sqrt{I} .$

Facts & Assumptions

Given: The Axiom of Choice, an algebraically closed field $k$ , and an ideal $I \subseteq k [x_{1}, \dots, x_{n}]$ .

[L1]

The radical $\sqrt{I}$ consists of the polynomials whose some positive power lies in $I$ (The radical of an ideal).

[L2]

If $f$ vanishes on $V (I)$ , then the auxiliary ideal $I + (1 - y f)$ has empty zero locus (The Rabinowitsch auxiliary ideal has no common zero).

[L3]

Under the same hypothesis, the auxiliary ideal is the unit ideal (The auxiliary ideal is the unit ideal).

[L4]

A unit-ideal identity for the auxiliary ideal yields a power of $f$ in $I$ (Substituting y = 1/f and clearing denominators yields a power of f in I).

Proof

technique · direct

1.1L1given

If $f \in \sqrt{I}$ , then [L1] gives $f^{N} \in I$ for some $N \geq 1$ . For every $a \in V (I)$ we have $f (a)^{N} = 0$ , and a field has no nonzero nilpotents, so $f (a) = 0$ . Thus $f \in I (V (I))$ , proving $\sqrt{I} \subseteq I (V (I))$ .

1.2L1L2L3L4

Conversely, let $f \in I (V (I))$ , so $f$ vanishes on $V (I)$ . Then [L2] and [L3] give a unit-ideal identity for $I + (1 - y f)$ , and [L4] turns it into $f^{N} \in I$ for some $N \geq 1$ . By [L1], this means $f \in \sqrt{I}$ . Therefore $I (V (I)) \subseteq \sqrt{I}$ .

2.1step 1.1step 1.2∎

The two inclusions from steps 1.1 and 1.2 yield $I (V (I)) = \sqrt{I}$ .

Depends on

Used by

Dependency tree · two levels

11 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, A Primer of Commutative Algebra, v4.03, Theorem 13.10 (standard reference, not scraped)
Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Theorem (15.7) (standard reference, not scraped)