CorollaryStatement: 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.

Every $1 + u$ with $u \in x R ⟦ x ⟧$ has a unique $k$ th root with constant coefficient $1$ in a commutative $Q$ -algebra

Statement

Let $R$ be a commutative $Q$ -algebra, $u \in x R ⟦ x ⟧$ , and $k \geq 1$ . There is a unique $v \in 1 + x R ⟦ x ⟧$ such that

$v^{k} = 1 + u,$

namely $v = (1 + u)^{1 / k}$ . When $u = 0$ , this unique root is $1$ .

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

In a commutative $Q$ -algebra, formal $\exp$ and $\log$ are inverse group homomorphisms on $x R ⟦ x ⟧$ and $1 + x R ⟦ x ⟧$ , and for $u \in x R ⟦ x ⟧$ and $c, d \in R$ the exponent-addition and exponent-multiplication laws hold (Formal $\exp$ and $\log$ are inverse homomorphisms and formal binomial powers obey the expected addition laws).

Proof

technique · apply the formal logarithm

1.1

The power law gives $((1 + u)^{1 / k})^{k} = (1 + u)^{1} = 1 + u$ , so the stated series is a root with constant coefficient $1$ .

givenF1

1.2

If $v \in 1 + x R ⟦ x ⟧$ and $v^{k} = 1 + u$ , the logarithm addition law gives $k \log v = \log (1 + u)$ . Since $k$ is invertible in a $Q$ -algebra, $\log v = (1 / k) \log (1 + u)$ ; applying $\exp$ gives $v = (1 + u)^{1 / k}$ . This proves uniqueness.

givenF1

2.1

For $u = 0$ , the construction is $\exp (0) = 1$ , and step 1.2 excludes any other constant-one root.

step 1.1step 1.2givenF1∎

Depends on

Used by

Dependency tree · two levels

8 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

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

Every 1+u1+u with u∈xR⟦x⟧u∈xR[[x]] has a unique kkth root with constant coefficient 11 in a commutative QQ-algebra