TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31

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.

Valuation rings are integrally closed

Statement

Every valuation ring is an integrally closed domain.

Facts & Assumptions

Given: A valuation ring $V$ contained in a field $K$ .

[L1]

A domain is integrally closed when every element of its field of fractions integral over it already lies in the domain (Integral closure in an extension ring and integrally closed domains).

[F1]

A valuation ring is a subring $V \subseteq K$ such that for each $x \in K^{\times}$ , at least one of $x$ and $x^{- 1}$ lies in $V$ (Valuation rings).

[L2]

A valuation ring is local, and its nonunits form the unique maximal ideal (A valuation ring is local).

[A1]

Any subring of a field is a domain, and its field of fractions embeds in that field.

Proof

technique · direct

1.1

Let $x$ be an element of the field of fractions of $V$ that is integral over $V$ . By [A1], regard $x$ as an element of $K$ . If $x \notin V$ , then [F1] gives $x^{- 1} \in V$ . This element is not a unit of $V$ , because a unit inverse would put $x$ back in $V$ . Hence [L2] places $x^{- 1}$ in the maximal ideal $m$ of $V$ .

F1L2A1given

2.1

Choose a monic equation $x^{n} + a_{n - 1} x^{n - 1} + \dots + a_{0} = 0$ with $a_{i} \in V$ . Multiplying by $x^{- n}$ gives $1 + a_{n - 1} x^{- 1} + \dots + a_{0} x^{- n} = 0$ . Since $x^{- 1} \in m$ and $m$ is an ideal, every term except $1$ lies in $m$ . Therefore $1 \in m$ , contradicting maximality.

step 1.1algebra

3.1

So $x \in V$ . By [L1], this proves that $V$ is integrally closed; by [A1], it is also a domain.

L1step 2.1A1∎

Depends on

Used by

Equivalent characterizations of a DVR Theorem

Dependency tree · two levels

6 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

Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Exercise (26.5) (standard reference, not scraped)
M. Mustata, Commutative Algebra, Section 8.1 (standard reference, not scraped)