TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

The binomial theorem over an arbitrary commutative ring

Statement

Let $R$ be a commutative ring. For all $x, y \in R$ and $n \in N$ ,

$(x + y)^{n} = \sum_{k = 0}^{n} (\binom{n}{k}) x^{k} y^{n - k} .$

The natural-number coefficients act by repeated addition. The formula includes $n = 0$ .

Facts & Assumptions

Given: A commutative ring $R$ , elements $x, y \in R$ , and a natural number $n$ .

[L1]

Multiplication in a commutative ring is commutative and distributes over addition (Commutative ring).

[L2]

The binomial coefficient $(\binom{n}{k})$ counts the $k$ -element subsets of an $n$ -element set, with $(\binom{n}{0}) = (\binom{n}{n}) = 1$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[L3]

Natural powers satisfy $z^{0} = 1$ and $z^{r + 1} = z^{r} z$ (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ ).

[L4]

Pascal's identity is $(\binom{n + 1}{k + 1}) = (\binom{n}{k}) + (\binom{n}{k + 1})$ (Pascal's rule $(\binom{n + 1}{k + 1}) = (\binom{n}{k}) + (\binom{n}{k + 1})$ , and the hockey-stick identity $\sum_{i \leq n} (\binom{i}{k}) = (\binom{n + 1}{k + 1})$ ).

Proof

technique · induction

1.1

For $n = 0$ , both sides are $1$ : the left by [L3], and the right is the sole term $(\binom{0}{0}) x^{0} y^{0} = 1$ .

baseL2L3

1.2

Assume the formula holds for $n$ .

2.1

Multiply the inductive formula by $x + y$ , distribute using [L1], and reindex to obtain the coefficient $(\binom{n}{k - 1}) + (\binom{n}{k})$ on $x^{k} y^{n + 1 - k}$ for each interior $k$ .

step 1.2L1L3algebra

3.1

By [L4] these interior coefficients are $(\binom{n + 1}{k})$ , and [L2] supplies the two endpoint coefficients $1$ . Thus the formula holds for $n + 1$ .

step 2.1L2L4algebra

4.1

Induction proves the identity for every natural $n$ .

step 1.1step 3.1discharge-induction∎

Depends on

Used by

Frobenius x↦ xᵖ is an injective endomorphism in characteristic p, and an automorphism for finite fields Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 75 results over 22 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

A. W. Knapp, Basic Algebra, 2nd ed., Chapter IX, Section 3 (standard reference, not scraped)