LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-sol)audited 2026-09-27

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.

A field has only the zero ideal and itself, hence is Noetherian

Statement

Let $K$ be a field (Field). Then the only ideals of $K$ are the zero ideal $(0)$ and $K$ itself (Left, right and two-sided ideals, The ideal generated by a subset and principal ideals); consequently every ideal of $K$ is finitely generated, and $K$ is a Noetherian ring (Noetherian commutative rings and modules). No choice principle is used.

Facts & Assumptions

Given: A field $K$ and an ideal $I \subseteq K$ .

[F1]

Field: in a field every nonzero element $a$ has a multiplicative inverse $a^{- 1}$ with $a a^{- 1} = 1$ , and $1 \neq 0$ .

[F2]

Left, right and two-sided ideals: an ideal $I \subseteq K$ is an additive subgroup closed under multiplication by elements of $K$ , so $r a \in I$ for all $r \in K$ , $a \in I$ ; hence $I = K$ as soon as $1 \in I$ .

[F3]

The ideal generated by a subset and principal ideals: for $a \in K$ the ideal $(a)$ is the intersection of all ideals containing $a$ ; in particular $(0) = {0}$ is generated by $0$ and $K = (1)$ is generated by $1$ , so both are generated by a single element.

[F4]

Noetherian commutative rings and modules: the ring $K$ is Noetherian if and only if every ideal of $K$ is finitely generated; the definition states the two conditions as equivalent.

Proof

technique · direct

1.1

A nonzero ideal is everything: if $I \neq (0)$ choose $a \in I$ with $a \neq 0$ ; by [F1] $a$ is invertible with inverse $a^{- 1} \in K$ , and since $I$ is closed under multiplication by elements of $K$ , $1 = a^{- 1} a \in I$ by [F2]; then $x = x \cdot 1 \in I$ for every $x \in K$ by [F2] again, so $I = K$ .

F1F2given

2.1

The ideal list: by step 1.1 every ideal of $K$ is either $(0)$ or $K$ ; the zero ideal is generated by the single element $0$ and $K = (1)$ is generated by the single element $1$ , so every ideal of $K$ is finitely generated.

step 1.1F3

3.1

Conclusion: by step 2.1 every ideal of $K$ is finitely generated, so [F4] makes $K$ a Noetherian ring. The argument used only the field axioms, the ideal axioms and the two-element list of ideals, so it invokes no choice principle.

step 2.1F4given∎

Depends on

Used by

Dependency tree · two levels

12 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

Stacks Project, Algebra, Section 10.31 (tag 00FM) and Lemma 10.31.3 (tag 00FO) (standard reference, not scraped)