LemmaStatement: 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.

Substituting y = 1/f and clearing denominators yields a power of f in I

Statement

Let $k$ be a field, let $m \geq 1$ , let $I = (h_{1}, \dots, h_{m}) \subseteq k [x_{1}, \dots, x_{n}]$ , and let

1 = \sum_{i = 1}^{m} a_{i} (x, y) h_{i} (x) + b (x, y) (1 - y f (x))

be an identity in $k [x_{1}, \dots, x_{n}, y]$ . Then some power $f^{N}$ lies in $I$ .

Facts & Assumptions

Given: A field $k$ , an integer $m \geq 1$ , an ideal $I = (h_{1}, \dots, h_{m})$ in $R : = k [x_{1}, \dots, x_{n}]$ , a polynomial $f \in R$ , and a unit-ideal identity for $I + (1 - y f)$ .

[L1]

Localization at a multiplicative set adjoins inverses of its elements (Multiplicative subsets and the localisation $S^{- 1} R$ as equivalence classes of fractions).

[L2]

Localization is a ring and supports substitution of equal fractions (The localisation relation is an equivalence relation and fraction arithmetic is well defined).

[L3]

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

Proof

technique · direct

1.1

If $f = 0$ , then $f^{1} = 0 \in I$ , so the conclusion is immediate. Hence we may assume $f \neq 0$ .

givenalgebra

2.1

The hypothesis $m \geq 1$ excludes the empty generating-family case, so the finite maximum used below is defined. Let $S = {1, f, f^{2}, \dots} \subseteq R$ . By [L1] and [L2], in the localized ring $S^{- 1} R$ the element $f / 1$ is invertible with inverse $1 / f$ .

L1L2step 1.1givenalgebra

3.1

Substitute $y = 1 / f$ into the displayed identity and view the coefficients in $S^{- 1} R$ . The term $1 - y f$ becomes $0$ , so we obtain $1 = \sum_{i = 1}^{m} a_{i} (x, 1 / f) h_{i} (x)$ in $S^{- 1} R$ . Each coefficient $a_{i} (x, 1 / f)$ is a fraction $r_{i} / f^{e_{i}}$ .

L2step 2.1algebra

4.1

Let $N = \max_{i} e_{i}$ . Multiplying the equality of step 3.1 by $f^{N}$ in the localization gives $\frac{f^{N} - \sum_{i = 1}^{m} r_{i} f^{N - e_{i}} h_{i}}{1} = 0.$ By the localization equality criterion, some power $f^{M} \in S$ annihilates the numerator in $R$ . Since $R = k [x_{1}, \dots, x_{n}]$ is an integral domain and step 1.1 gives $f \neq 0$ , this forces $f^{N} = \sum_{i = 1}^{m} r_{i} f^{N - e_{i}} h_{i}$ already in $R$ . The right-hand side lies in $I$ , so $f^{N} \in I$ .

L2step 1.1step 3.1algebra

5.1

Thus a power of $f$ belongs to $I$ . The existence of the starting identity is exactly what [L3] supplies in the Nullstellensatz application.

L3step 4.1∎

Depends on

Used by

Strong Nullstellensatz: I(V(I)) equals the radical of I Corollary
A small Rabinowitsch identity written out completely Example

Dependency tree · two levels

9 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)