Existing in Mathlib · Algebra

Binomial Theorem

In any commutative semiring, expanding the nth power of x + y gives a finite sum with one term for each m from 0 through n: choose m of the n factors to contribute x, let the others contribute y, and weight the resulting monomial by n.choose m.

binomial theorem
commutative semirings
finite sums
binomial coefficients
natural powers
combinatorial choice

Exact theorem

Exact Mathlib statement

theorem add_pow [CommSemiring R] (x y : R) (n : ℕ) : (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * n.choose m

The theorem at a glance

The binomial theorem at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

An ivory binomial-theorem poster places the exact finite range sum above a three-factor combinatorial expansion: eight three-token choices are gathered into four bounded groups of sizes one, three, three, and one according to how many factors contribute x. — The n-fold product of x + y becomes a finite sum after choices are grouped by the number m of factors contributing x.

Statement structure

From hypotheses to conclusion

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

Scientific figure illustrating: Three paired choice gates feed eight three-token bands into four finite aggregation medallions. — Exactly eight three-token outcomes separate into the finite group sizes one, three, three, and one.

Why it matters

A mathematical landmark

The binomial theorem is a foundational bridge between algebraic expansion and combinatorial counting. Mathlib's add_pow states it at the natural generality of a commutative semiring and makes the finite index range, complementary exponents, and binomial coefficient completely explicit.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This page indexes Mathlib's commutative-semiring binomial theorem add_pow. For x and y in a commutative semiring and n in ℕ, it gives one finite sum indexed by range (n + 1), with summand x ^ m * y ^ (n - m) * n.choose m. It is not an analytic infinite-series statement, does not extend the exponent beyond natural numbers, and does not claim the formula for arbitrary noncommuting elements.

The selected declaration is a finite algebraic identity for natural powers; it does not state an infinite binomial series or a convergence theorem.
The theorem assumes a commutative semiring. It does not claim the formula for arbitrary noncommuting x and y; the nearby Commute.add_pow declaration handles an explicitly commuting pair.
The finite sum is indexed by m in range (n + 1), and its summand retains the exact exponents m and n - m together with n.choose m.
The combinatorial visual explanation is not a replacement for the full finite-sum statement, and generated visuals are not proof evidence.
ProofAtlas is indexing an existing upstream Mathlib theorem, not presenting new ProofAtlas mathematics.

Source and local evidence

Where the theorem comes from

Existing declaration: add_pow in mathlib
Relationship: The checked artifact is the upstream declaration itself
Local Lean evidence: artifact.library.mathlib.binomial-theorem.v001
Source: Open the pinned upstream reference