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

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.

For every field $F$ , $F [x]$ is a Euclidean domain with degree as Euclidean function

Statement

For every field $F$ , the ring $F [x]$ is a Euclidean domain with Euclidean function $δ (f) = \deg f$ on nonzero polynomials.

Facts & Assumptions

Given: A field $F$ .

[L1]

A polynomial ring over an integral domain is an integral domain (A polynomial ring over an integral domain is an integral domain).

[L2]

For $f \in F [x]$ and $0 \neq g \in F [x]$ , there are $q, r$ with $f = q g + r$ and $r = 0$ or $\deg r < \deg g$ (Division algorithm for polynomials over a field).

[L3]

A Euclidean domain is an integral domain with a natural-valued function on nonzero elements satisfying exactly that division condition (Euclidean domain and Euclidean function).

[L4]

A field is an integral domain because nonzero elements are invertible and $0 \neq 1$ (Field).

Proof

technique · direct

1.1

By [L4] and [L1], $F [x]$ is an integral domain.

givenL1L4

2.1

Degree is natural-valued on nonzero polynomials, and [L2] supplies the division condition of [L3], so $F [x]$ is Euclidean with $δ = \deg$ .

step 1.1L2L3∎

Depends on

Used by

For every field F, F[x] is a principal ideal domain Corollary
polynomial local regularity fibre step Lemma

Dependency tree · two levels

10 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

Neil Donaldson, Math 120B Notes, Section 23 (standard reference, not scraped)

For every field FF, F[x]F[x] is a Euclidean domain with degree as Euclidean function