CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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 a field $K$ , $K ⟦ x ⟧$ is a domain and its nonunits form the unique maximal ideal $x K ⟦ x ⟧$

Statement

If $K$ is a field, then $K ⟦ x ⟧$ is an integral domain. Its set of nonunits is exactly

$x K ⟦ x ⟧ = {f \in K ⟦ x ⟧ : [x^{0}] f = 0},$

which is the unique maximal ideal of $K ⟦ x ⟧$ .

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

A field has $0 \neq 1$ , commutative multiplication, and an inverse for every nonzero element (Field).

[F2]

Over an integral domain, formal order is additive on products with the $+ \infty$ convention, and the power-series ring is an integral domain (Formal order is non-Archimedean under sums and additive under products over a domain).

[F3]

A formal power series is a unit exactly when its constant coefficient is a unit (A formal power series is a unit exactly when its constant coefficient is a unit).

[F4]

Multiplication by $x^{k}$ shifts coefficients: $[x^{n}] (x^{k} f) = [x^{n - k}] f$ for $k \leq n$ and is $0$ for $k > n$ (Coefficient extraction is $R$ -linear, separates formal series, shifts under multiplication by $x^{k}$ , and converts products to finite convolution).

[F5]

A maximal ideal is a proper ideal with no proper ideal strictly between it and the whole ring (Prime ideals and maximal ideals in a commutative ring).

Proof

technique · identify the nonunits and test maximality

1.1

A field is a nonzero integral domain, so exact order additivity shows that a product of two nonzero series is nonzero. Thus $K ⟦ x ⟧$ is a domain.

givenF1F2

1.2

The unit criterion says that a series is a nonunit exactly when its constant coefficient is $0$ . The shift formula says these are exactly the multiples of $x$ : for such $f$ , define $g$ by $[x^{n}] g = [x^{n + 1}] f$ and obtain $f = x g$ . This set is a proper ideal because $1$ has constant coefficient $1 \neq 0$ .

givenF3F4

2.1

If an ideal strictly contains $x K ⟦ x ⟧$ , it contains a series with nonzero constant coefficient, hence a unit, and therefore is the whole ring. Thus $x K ⟦ x ⟧$ is maximal. Conversely, every proper ideal contains no unit, so every maximal ideal is contained in the set of nonunits $x K ⟦ x ⟧$ and hence equals it by maximality.

step 1.2givenF3F5

3.1

Steps 1.1-2.1 prove the domain claim and identify the unique maximal ideal, including the zero series and constant-series cases.

step 1.1step 1.2step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 28 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Benjamin Sambale, An Invitation to Formal Power Series (standard reference, not scraped)

For a field KK, K⟦x⟧K[[x]] is a domain and its nonunits form the unique maximal ideal xK⟦x⟧xK[[x]]