TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

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

Statement

Let $R$ be a commutative ring and $f = \sum_{n \geq 0} a_{n} x^{n} \in R ⟦ x ⟧$ . Then $f$ is a unit in $R ⟦ x ⟧$ if and only if $a_{0}$ is a unit in $R$ .

When $a_{0}$ is a unit, the inverse $g = \sum_{n \geq 0} b_{n} x^{n}$ is unique and is determined by

$b_{0} = a_{0}^{- 1}, b_{n} = - a_{0}^{- 1} \sum_{i = 1}^{n} a_{i} b_{n - i} (n \geq 1) .$

The criterion also holds in the zero ring.

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

Product coefficients satisfy $[x^{n}] (f g) = \sum_{i = 0}^{n} [x^{i}] f [x^{n - i}] g$ (Coefficient extraction is $R$ -linear, separates formal series, shifts under multiplication by $x^{k}$ , and converts products to finite convolution).

[F2]

Two formal series are equal if and only if all their coefficients are equal (Coefficient extraction is $R$ -linear, separates formal series, shifts under multiplication by $x^{k}$ , and converts products to finite convolution).

[F3]

An element $u$ is a unit exactly when there is $v$ with $u v = 1 = v u$ (The units of a ring are the invertible elements of its multiplicative monoid, and $R^{\times}$ is a group under multiplication; $0 \in R^{\times}$ only in the zero ring).

[F4]

Zero is a unit exactly in the zero ring (The units of a ring are the invertible elements of its multiplicative monoid, and $R^{\times}$ is a group under multiplication; $0 \in R^{\times}$ only in the zero ring).

Proof

technique · solve the inverse equations recursively

1.1givenF1F3

If $f g = 1$ , constant-coefficient extraction gives $a_{0} [x^{0}] g = 1$ . Commutativity gives the reverse product too, so $a_{0}$ is a unit.

1.2givenF1F2

Conversely suppose $a_{0}$ is a unit and define $b_{n}$ by the displayed recursion. The coefficient of $f g$ at $0$ is $a_{0} b_{0} = 1$ . For $n \geq 1$ it is $a_{0} b_{n} + \sum_{i = 1}^{n} a_{i} b_{n - i} = 0$ . Hence $f g = 1$ by extensionality, and commutativity gives $g f = 1$ .

2.1step 1.1step 1.2givenF3F4

Any inverse must satisfy the same constant equation and then, successively, the same equation for each $b_{n}$ ; multiplication by $a_{0}^{- 1}$ makes every coefficient unique. In the zero ring, $0 = 1$ and the unit theorem makes the same recursion and equivalence valid.

3.1step 1.1step 1.2step 2.1∎

Steps 1.1 and 1.2 prove both directions, while step 2.1 proves uniqueness and the boundary case.

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources