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.

✓ 17 results · all verified · 15 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Finite Counting, Factorials and Binomial Coefficients

1 · Prerequisites

2 · Summary

Objective. This page builds finite counting from the ground up: what $∣ A ∣$ means, the two rules that every count is assembled from, and the factorials and binomial coefficients they produce. It ends with the binomial and multinomial theorems and with stars and bars. Everything is proved from this page's declared prerequisites — the countability page and the page on roots and rational powers — together with the naturals and the ordered-field foundations below them; nothing is imported from later in the reading order.

The starting point is The cardinality $∣ A ∣$ of a finite set. A set is finite when it is equinumerous with a natural number, and the pigeonhole principle says it is equinumerous with exactly one, so $∣ A ∣$ names a single natural number. Four consequences are proved there and used constantly: $∣ n ∣ = n$ , $∣ A ∣ = 0$ exactly for the empty set, transport of cardinality along a bijection, and the equivalence of $∣ A ∣ = ∣ B ∣$ with $A \approx B$ . The workhorse that follows, A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , says that a subset of a finite set is finite with no larger cardinality, that equal cardinality forces equality of the sets, and that an injection or a surjection of a finite set onto itself is a bijection. That last clause is where finiteness is spent; the successor map on $N$ shows what happens without it.

Several items on this page exist because of a gap in the published library, and it is worth saying which. The finite sums already in the library are real valued: Finite sums and finite products, by recursion opens with a sequence $a : N \to R$ . Every count on this page is a natural number, so the sum rule, the row sums of Pascal's triangle, the condition $\sum_{i} k_{i} = n$ on a multinomial coefficient and the stars-and-bars count all need a sum that stays in $N$ . That is Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ , built by the same recursion, together with Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , which proves the usual laws and the bridge $ι (\sum^{N}) = \sum^{R} ι$ and the injectivity of $ι$ . Those two clauses are the licence used throughout: an identity between counts may be proved in $R$ , where subtraction and division exist, and carried back. The third minted item is A finite sum is unchanged by a permutation of its index range: $\sum_{k < n} a_{π (k)} = \sum_{k < n} a_{k}$ for every bijection $π : n \to n$ . The published law list has additivity, scaling, splitting, monotonicity, telescoping and the product laws, and no permutation-invariance clause; without one, the sum $\sum_{i \in S} a_{i}$ over a finite index set is not well posed. It is proved here for all four of $(R, +)$ , $(R, \cdot)$ , $(N, +)$ , $(N, \cdot)$ by a single argument, and The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form is then well defined, with an explicit bridge back to the sum over an initial segment.

The two counting rules follow. The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition splices two enumerations into one; disjointness is used at exactly one step, the injectivity of the splice, and that step is named so the false statement on the companion page can point at it. The same splice, used as an enumeration, splits a sum along a partition of its index set, which is what the multinomial theorem later needs. The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ then counts $A \times B$ by slicing it over $B$ and adding, which needs no arithmetic at all, and iterates to a finite product of sets. Exponentiation of naturals is minted in Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ , again because Integer powers $a^{m}$ is real valued, and it carries the bridge $ι (m^{n}) = ι (m)^{n}$ and the agreement $0^{0} = 1$ . With it, The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ gives $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ , both degenerate cases included, and $∣ P (A) ∣ = 2^{∣ A ∣}$ for finite $A$ gives $∣ P (A) ∣ = 2^{n}$ together with $n < 2^{n}$ , deduced from Cantor's theorem rather than left beside it.

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ defines $n!$ and $n^{\underline{k}}$ by recursion inside $N$ . $0! = 1$ is the base clause of that recursion, not an imported convention: the monoid version of the empty product comes later in the reading order, so it could not be cited here even if one wanted to. The agreement with the empty product is then proved, and so is $ι (n!) = \prod_{j < n} ι (j + 1)$ , which is what keeps this factorial and the real-valued one used elsewhere in the library a single object. The number of injections from a $k$ -element set into an $n$ -element set is $n^{\underline{k}}$ counts injections as $n^{\underline{k}}$ , with both boundary regimes checked, and A finite set $A$ with $∣ A ∣ = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality gets $n!$ as the case $k = n$ . That theorem is stated about a set of bijections, with no group vocabulary anywhere, because the symmetric group is later in the reading order; it is on this page rather than among the examples so that a later page may cite it.

The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ defines $(\binom{n}{k})$ as the count $∣ [n]^{k} ∣$ of $k$ -element subsets. Integrality is then free and the familiar quotient is a theorem: $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ counts the bijections of $n$ twice, once directly and once by the image of an initial segment, and gets $(\binom{n}{k}) k! (n - k)! = n!$ , the relation $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient formula in $R$ , and the symmetry $(\binom{n}{k}) = (\binom{n}{n - k})$ by complementation. 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})$ follows by splitting the $k$ -subsets according to whether they contain a fixed point, and carries the hockey-stick identity as its second clause. A finite set with $n$ elements has exactly $(\binom{n}{2})$ two-element subsets, and $2 (\binom{n}{2}) = n (n - 1)$ records the count of unordered pairs, $2 (\binom{n}{2}) = n (n - 1)$ , checked at $n = 0$ and $n = 1$ ; it is stated purely as a count, since no graph is defined anywhere in the library at this point.

The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ is proved by induction from Pascal's rule. It is stated in $R$ , with the coefficient written $ι (\binom{n}{k})$ , because a binomial coefficient is a natural number and not an element of the field; the commutative-ring version is a separate statement, to be made where rings exist. $\sum_{k < n + 1} (\binom{n}{k}) = 2^{n}$ , and $\sum_{k < n + 1} (- 1)^{k} ι ⁣ (\binom{n}{k}) = 0$ for $n \geq 1$ draws the row sum $2^{n}$ , proved twice on purpose, once by partitioning the power set and once through the theorem, and the alternating row sum, which is $0$ only for $n \geq 1$ : at $n = 0$ the sum is $(\binom{0}{0}) = 1$ , and that is exactly where $(- 1 + 1)^{n} = 0^{n}$ stops being $0$ . Vandermonde's identity $(\binom{m + n}{k}) = \sum_{i < k + 1} (\binom{m}{i}) (\binom{n}{k - i})$ is a double count over a disjoint union, chosen in preference to generating functions and to coefficient comparison, both of which need machinery far later in the reading order.

The last block generalises. The multinomial coefficient $(\binom{n}{k_{0}, \dots, k_{m - 1}})$ as the number of ordered partitions of an $n$ -set into blocks of prescribed sizes counts the colourings of a finite set with prescribed fibre sizes, the condition $\sum_{i} k_{i} = n$ being part of the definition rather than a side remark, and The multinomial coefficient equals $n! / \prod_{i < m} k_{i}!$ , and $(x_{0} + \dots + x_{m - 1})^{n} = \sum ι ⁣ (\binom{n}{k}) \prod_{i < m} x_{i}^{k_{i}}$ in $R$ gives both the closed formula $(\binom{n}{k}) \prod_{i} k_{i}! = n!$ and the expansion of a power of a sum, its outer sum indexed by the finite set of tuples summing to $n$ . Compositions and weak compositions of a natural number into a fixed number of parts names those tuples and records the counts at $m = 0$ , and For $m \geq 1$ the number of weak compositions of $n$ into $m$ parts is $(\binom{n + m - 1}{m - 1})$ , and the number of compositions is $(\binom{n - 1}{m - 1})$ for $n \geq 1$ computes them: $(\binom{n + m - 1}{m - 1})$ weak compositions for $m \geq 1$ , and $(\binom{n - 1}{m - 1})$ compositions for $m \geq 1$ and $n \geq 1$ . The stars-and-bars bijection is exhibited explicitly and shown injective; surjectivity is read off from the count, which spares an appeal to the increasing enumeration of an arbitrary subset. Conventions fixed on this page, and what counting is deliberately not done here closes the page with every convention it fixes and with what is deliberately left to later pages, inclusion and exclusion among them.

Two habits are enforced throughout. Every sum, product and index range is checked at its first index, because $N$ contains $0$ here. Three results carry a hypothesis for that reason alone: the alternating row sum needs $n \geq 1$ , the weak-composition count needs $m \geq 1$ and the composition count needs $n \geq 1$ . The first two have a matching false statement on the companion page; the third is recorded in the theorem's own Statement. And every count is kept in $N$ , with $ι$ written whenever a count is used inside $R$ , so that the two sides of an identity always live in the same set.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The cardinality $∣ A ∣$ of a finite set

Definition

Throughout this page $N$ is the set of von Neumann naturals (The natural numbers $N$ (von Neumann)): $0 = \emptyset$ , $σ (n) = n \cup {n}$ , and $n = {m \in N : m < n}$ is itself the set of its predecessors, the order being the additive order of Order on the natural numbers identified with membership in On $N$ the order is membership: $m < n ⟺ m \in n$ . Write $A \approx B$ when a bijection $A \to B$ exists (Equinumerous sets, $A \approx B$ and $A ⪯ B$ , Injection, surjection, bijection). A set $A$ is finite when $A \approx n$ for some $n \in N$ (Finite, countably infinite, countable, uncountable).

Definition. Let $A$ be a finite set. Then there is exactly one $n \in N$ with $A \approx n$ , and we write

$∣ A ∣ : = that n,$

the cardinality, or number of elements, of $A$ . The notation $∣ A ∣$ is defined for finite $A$ only, and its value is a natural number.

Why exactly one, which is the whole content of the definition. At least one such $n$ exists: that is literally what " $A$ is finite" says. At most one exists: if $A \approx n$ and $A \approx m$ with $n, m \in N$ , then $n \approx A$ , because the inverse of a bijection is a bijection, and hence $n \approx m$ , because a composition of bijections is a bijection (Injection, surjection, bijection); and $n \approx m$ forces $n = m$ by claim 3 of The pigeonhole principle on $N$ . So $∣ A ∣$ names a single natural number and not a family of choices.

Four consequences, proved here because everything on this page uses them.

(a) $∣ n ∣ = n$ for every $n \in N$ . The identity map ${i d}_{n}$ is a bijection $n \to n$ , so $n \approx n$ ; thus $n$ is finite and the unique natural equinumerous with it is $n$ itself.

(b) $∣ \emptyset ∣ = 0$ , and a finite $A$ satisfies $∣ A ∣ = 0$ if and only if $A = \emptyset$ . Since $0 = \emptyset$ , part (a) gives $∣ \emptyset ∣ = 0$ . Conversely, if $∣ A ∣ = 0$ then there is a bijection $f : A \to \emptyset$ ; were some $a \in A$ , the value $f (a)$ would be an element of $\emptyset$ , and $\emptyset$ has none, so $A = \emptyset$ .

(c) Transport along a bijection. If $A$ is finite and $f : A \to B$ is a bijection, then $B$ is finite and $∣ B ∣ = ∣ A ∣$ . Indeed $B \approx A$ through $f^{- 1}$ and $A \approx ∣ A ∣$ , so $B \approx ∣ A ∣$ by transitivity.

(d) Equality of cardinalities is equinumerosity. For finite $A$ and $B$ : $∣ A ∣ = ∣ B ∣$ if and only if $A \approx B$ . If the cardinalities agree then $A \approx ∣ A ∣ = ∣ B ∣ \approx B$ ; conversely $A \approx B$ gives $∣ B ∣ = ∣ A ∣$ by (c).

Remarks

$N$ contains $0$ here, and that is not a detail. Every index range on this page starts at $0$ , a one-element set has cardinality $1 = {0}$ , and $∣ A ∣$ is never a positive-integer-only object. A statement about $∣ A ∣$ that is true only for $∣ A ∣ \geq 1$ must say so.
$∣ A ∣$ is a natural number, not a cardinal number. The theory of cardinals (Cardinal (initial ordinal) and cardinality ↗) is developed much later in the library and nothing here uses it, or any cardinal arithmetic: the pointer is orientation only. What makes the notation legitimate at this point in the reading order is exactly claim 3 of The pigeonhole principle on $N$ , and nothing more.
What the definition does not supply. It asserts that some bijection $A \to ∣ A ∣$ exists; it does not single one out, and nothing in the library does. Two sets can have equal cardinality with no distinguished bijection between them, which is the point of the counterexample on this page's companion.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$

Statement

Let $A$ be a finite set (Finite, countably infinite, countable, uncountable) and let $B \subseteq A$ . Then:

$B$ is finite;
$∣ B ∣ \leq ∣ A ∣$ (The cardinality $∣ A ∣$ of a finite set);
$∣ B ∣ = ∣ A ∣$ if and only if $B = A$ ;
every injection $f : A \to A$ is a bijection, and every surjection $f : A \to A$ is a bijection.

Clause 3 is the finite form of the Dedekind statement: a finite set is not equinumerous with a proper subset of itself. Clause 4 is its working form, and finiteness is exactly the hypothesis that fails in general: the successor map is an injection of $N$ into itself that is not surjective, which is the false statement recorded on this page's companion.

Facts & Assumptions

Given: A finite set $A$ , its cardinality $n : = ∣ A ∣$ , and a subset $B \subseteq A$ . Throughout, $σ (n) = n \cup {n}$ and $σ (n) = n + 1$ , the latter because $n + σ (0) = σ (n + 0) = σ (n)$ (Addition of natural numbers).

[L1]

Induction: a property holding at $0$ and inherited by successors holds at every natural (The principle of mathematical induction).

[L2]

On $N$ the order is membership: $m < n ⟺ m \in n$ , $m \leq n ⟺ m \subseteq n$ , and $n = {m \in N : m < n}$ ; also $m < σ (n) ⟺ m \leq n$ (On $N$ the order is membership: $m < n ⟺ m \in n$ , Order on the natural numbers, The natural numbers $N$ (von Neumann)). By the definition of the strict order, $m < m$ is impossible.

[L3]

Cardinality (The cardinality $∣ A ∣$ of a finite set): $∣ A ∣$ is the unique natural with $A \approx ∣ A ∣$ ; $∣ n ∣ = n$ ; $∣ \emptyset ∣ = 0$ ; and if $A$ is finite and $A \approx B$ then $B$ is finite with $∣ B ∣ = ∣ A ∣$ (transport).

[L4]

Maps and equinumerosity (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ B$ , Finite, countably infinite, countable, uncountable): $A$ is finite when $A \approx m$ for some $m \in N$ ; the restriction of an injection to a subset of its domain is an injection; an injection is a bijection onto its image; inverses and composites of bijections are bijections; and $f^{- 1} [f [S]] = S$ for a bijection $f$ and $S$ contained in its domain.

[L5]

Order and successor: $k \leq n$ implies $σ (k) \leq σ (n)$ , and $σ (k) = σ (n)$ implies $k = n$ (Order is compatible with addition, Addition is cancellative, with $σ (m) = m + 1$ ).

[L6]

Discreteness: $m < n ⟺ σ (m) \leq n$ (Discreteness: $σ (n)$ is the immediate successor).

[L7]

Well-ordering: every nonempty subset of $N$ has a least element (The well-ordering principle).

Proof

technique · induction

1.1

The whole theorem rests on the special case where the ambient set is a natural number, which we call $(*)$ : for every $n \in N$ and every $B \subseteq n$ , the set $B$ is finite, $∣ B ∣ \leq n$ , and $∣ B ∣ = n$ implies $B = n$ . It is proved by induction on $n$ .

given

1.2

Base case $n = 0$ . Since $0 = \emptyset$ , a subset $B \subseteq 0$ satisfies $B = \emptyset = 0$ ; so $B$ is finite with $∣ B ∣ = 0 \leq 0$ , and $∣ B ∣ = 0$ indeed gives $B = 0$ .

baseL3L2

1.3

Inductive hypothesis. Fix $n \in N$ and assume $(*)$ holds for $n$ : every $C \subseteq n$ is finite with $∣ C ∣ \leq n$ , and $∣ C ∣ = n$ implies $C = n$ .

2.1

Let $B \subseteq σ (n) = n \cup {n}$ and put $B^{'} : = B \cap n$ , so that $B^{'} \subseteq n$ , and $B = B^{'}$ when $n \notin B$ while $B = B^{'} \cup {n}$ with $n \notin B^{'}$ when $n \in B$ . By the inductive hypothesis of step 1.3 the set $B^{'}$ is finite; write $k : = ∣ B^{'} ∣$ , so $k \leq n$ , and $k = n$ forces $B^{'} = n$ .

step 1.3L2

3.1

Case $n \notin B$ . Here $B = B^{'}$ is finite with $∣ B ∣ = k \leq n$ , and $k \leq n \leq σ (n)$ gives $∣ B ∣ \leq σ (n)$ ; moreover $∣ B ∣ = σ (n)$ is impossible, since $σ (n) = k \leq n$ would give $n < n$ by [L6], so the third assertion of $(*)$ holds vacuously in this case.

step 2.1L2L6

3.2

Case $n \in B$ . Choose a bijection $g : k \to B^{'}$ , which exists because $∣ B^{'} ∣ = k$ , and define $h : σ (k) \to B$ by $h (i) = g (i)$ for $i \in k$ and $h (k) = n$ ; the two clauses do not conflict, since $k \notin k$ . Then $h$ is injective, because $g$ is injective and takes its values in $B^{'} \subseteq n$ , so no value $g (i)$ equals $n$ ; and $h$ is surjective onto $B = B^{'} \cup {n}$ . Hence $B \approx σ (k)$ , so $B$ is finite with $∣ B ∣ = σ (k)$ .

step 2.1L3L4construct

4.1

In the case $n \in B$ we therefore have $∣ B ∣ = σ (k) \leq σ (n)$ , because $k \leq n$ ; and if $∣ B ∣ = σ (n)$ then $σ (k) = σ (n)$ , so $k = n$ , so $B^{'} = n$ and therefore $B = n \cup {n} = σ (n)$ .

step 2.1step 3.2L5

5.1

The two cases are exhaustive, so $(*)$ holds at $σ (n)$ whenever it holds at $n$ ; with the base case this gives $(*)$ for every $n \in N$ .

step 1.2step 1.3step 3.1step 4.1L1

6.1

Clauses 1 and 2 in general. Fix a bijection $u : A \to n$ , available since $n = ∣ A ∣$ . Then $u [B] \subseteq n$ , and the restriction of $u$ to $B$ is a bijection of $B$ onto $u [B]$ , so $B \approx u [B]$ . By $(*)$ the set $u [B]$ is finite with $∣ u [B] ∣ \leq n$ , hence $B$ is finite with $∣ B ∣ = ∣ u [B] ∣ \leq n = ∣ A ∣$ .

step 5.1L3L4

7.1

Clause 3. If $B = A$ then $∣ B ∣ = ∣ A ∣$ . Conversely assume $∣ B ∣ = ∣ A ∣ = n$ . Then $∣ u [B] ∣ = ∣ B ∣ = n$ by transport, so $u [B] = n$ by $(*)$ , and therefore $B = u^{- 1} [u [B]] = u^{- 1} [n] = A$ , because $u$ is a bijection of $A$ onto $n$ .

step 5.1step 6.1L3L4

8.1

Clause 4, the injective half. Let $f : A \to A$ be injective. Then $f$ is a bijection of $A$ onto its image $f [A] \subseteq A$ , so $∣ f [A] ∣ = ∣ A ∣$ by transport, and clause 3 gives $f [A] = A$ . Thus $f$ is surjective, hence a bijection.

step 7.1L3L4

9.1

Clause 4, the surjective half. Let $f : A \to A$ be surjective. For each $b \in A$ the set $u [f^{- 1} [{b}]] \subseteq n$ is nonempty, so it has a least element by [L7]; let $g (b)$ be the value of $u^{- 1}$ at that least element. No choice principle is used, since each $g (b)$ is determined by $b$ rather than selected. By construction $g (b) \in f^{- 1} [{b}]$ , that is $f (g (b)) = b$ for every $b$ ; and $g$ is injective, since $g (b) = g (b^{'})$ gives $b = f (g (b)) = f (g (b^{'})) = b^{'}$ . So $g$ is a bijection by step 8.1.

step 6.1step 8.1L4L7construct

10.1

Composing $f \circ g = {i d}_{A}$ on the right with $g^{- 1}$ gives $f = g^{- 1}$ , which is a bijection; so a surjection of $A$ onto itself is a bijection, and in particular an injection.

step 9.1L4

11.1

Clauses 1 and 2 are step 6.1, clause 3 is step 7.1, and clause 4 is steps 8.1 and 10.1, each resting on the induction that establishes $(*)$ .

step 5.1step 6.1step 7.1step 8.1step 10.1discharge-induction∎

Remarks

Where finiteness is spent. Only in $(*)$ , and there only through the base case $0 = \emptyset$ and the fact that removing the top point of $σ (n)$ leaves $n$ . Clause 4 then follows formally, which is why the failure of clause 4 for $N$ is a failure of finiteness and of nothing else.
The surjective half needs no choice. The obvious argument, "pick a preimage of each $b$ ", would need a choice function on the fibres. Transporting the fibres into $N$ and taking least elements replaces the choice by a determination, which is what The well-ordering principle is for.
Clause 2 is not the pigeonhole principle restated. The pigeonhole principle on $N$ is about injections between natural numbers, and it is what makes The cardinality $∣ A ∣$ of a finite set well posed in the first place; clause 2 compares the cardinalities of a set and a subset, and is proved here by induction directly.

DefinitionDefinition: AI-adaptedProof: AI-generatedverified 2026-08-02 (claude-opus-5)Open item page →

Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$

Definition

Let $a : N \to N$ , written $a_{k}$ for $a (k)$ , with addition and multiplication of natural numbers as in Addition of natural numbers and Multiplication of natural numbers. Finite sums and finite products of $a$ inside $N$ are defined by recursion on the upper index, which is legitimate by the recursion theorem (The recursion theorem).

That theorem produces a function of one variable, so the running index has to be carried inside the value. Apply it to the set $A = N \times N$ , the starting element $(0, 0)$ and the function $f (k, s) = (σ (k), s + a_{k})$ : there is a unique $g : N \to N \times N$ with

$g (0) = (0, 0), g (σ (n)) = f (g (n)) (n \in N) .$

Write $g (n) = (π_{1} (g (n)), S_{n})$ for its two coordinates.

The first coordinate is the index itself, and that is an induction, not an observation (The principle of mathematical induction). Indeed $π_{1} (g (0)) = 0$ ; and if $π_{1} (g (n)) = n$ then $g (σ (n)) = f (π_{1} (g (n)), S_{n}) = (σ (π_{1} (g (n))), S_{n} + a_{π_{1} (g (n))}) = (σ (n), S_{n} + a_{n})$ , so $π_{1} (g (σ (n))) = σ (n)$ . Only now may the second coordinates of the two displayed clauses be read off, and doing so gives

$S_{0} = 0, S_{σ (n)} = S_{n} + a_{n} .$

$S$ is moreover the unique function $N \to N$ with those two properties: if $S^{'}$ also has them then $n \mapsto (n, S_{n}^{'})$ satisfies the two clauses defining $g$ , hence equals $g$ by the uniqueness clause of The recursion theorem, so $S^{'} = S$ . We write

$\sum_{k < n} a_{k} : = S_{n} .$

The same construction with starting element $(0, 1)$ and $f (k, p) = (σ (k), p \cdot a_{k})$ , with the same induction on the first coordinate and the same uniqueness argument, gives the unique $P : N \to N$ with

$P_{0} = 1, P_{σ (n)} = P_{n} \cdot a_{n},$

and we write $\prod_{k < n} a_{k} : = P_{n}$ .

The empty sum is $0$ and the empty product is $1$ , by the base clause of the recursion and by nothing else: no convention is imported from anywhere.

Notation. We abbreviate $\sum_{k = 0}^{n} a_{k} : = \sum_{k < n + 1} a_{k}$ and likewise for products, using $σ (n) = n + 1$ . Only finitely many values of $a$ enter $\sum_{k < n} a_{k}$ , so the notation is also used for a list $a_{0}, \dots, a_{n - 1}$ of naturals given without reference to any extension to all of $N$ : extend the list by $a_{k} = 0$ (respectively $a_{k} = 1$ ) for $k \geq n$ and apply the definition. Where the two kinds of finite sum have to be told apart, we write $\sum^{N}$ and $\prod^{N}$ for the ones defined here and $\sum^{R}$ , $\prod^{R}$ for those of Finite sums and finite products, by recursion; elsewhere the ambient set is fixed by the terms being summed.

Truncated difference, fixed here for the whole page. For $m, n \in N$ we write $n - m$ for the unique $j \in N$ with $m + j = n$ when $m \leq n$ , and for $0$ when $n < m$ . Existence in the first case is the definition of $\leq$ (Order on the natural numbers) and uniqueness is commutativity with cancellation (Addition is commutative, Addition is cancellative). The two cases are exhaustive and mutually exclusive, since exactly one of $m < n$ , $m = n$ , $n < m$ holds (Trichotomy of the order on $N$ ), so the notation names a single natural number for every $m$ and $n$ . Every use of $n - m$ on this page is this operation; no negative number is ever formed, and where a statement is true only under $m \leq n$ that hypothesis is written out.

Remarks

Why a second finite sum is needed at all. Finite sums and finite products, by recursion defines $\sum_{k < n} a_{k}$ for a sequence of reals, and its value is a real number. Every count on this page is a natural number, so the sum rule, the row sums of Pascal's triangle, the condition $\sum_{i} k_{i} = n$ on a multinomial coefficient and the stars-and-bars count all need a sum that stays in $N$ . The two notions are related, not rival: the bridge $ι (\sum_{k < n}^{N} a_{k}) = \sum_{k < n}^{R} ι (a_{k})$ is proved in the next item, and it is what lets an identity between counts be read inside $R$ and back.
The monoid version, later. The same recursion is carried out in an arbitrary monoid in The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity ↗, which comes later in the reading order; $(N, +, 0)$ and $(N, \cdot, 1)$ are instances of it, and the agreement is immediate because the recursion clauses are identical. That pointer is orientation only: nothing here depends on it, and the notion defined above is complete as it stands.
$0$ is an index. $\sum_{k < n}$ runs over $k = 0, 1, \dots, n - 1$ , so $\sum_{k < 1} a_{k} = a_{0}$ and $\sum_{k < 0} a_{k} = 0$ . A claim about $\sum_{k < n} a_{k}$ must be checked at $n = 0$ , where it is a claim about $0$ , and a claim about $\prod_{k < n} a_{k}$ at $n = 0$ , where it is a claim about $1$ .

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$

Statement

Let $a, b : N \to N$ , let $c \in N$ , and let $m, n \in N$ , with $\sum^{N}$ and $\prod^{N}$ as in Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ and $\sum^{R}$ , $\prod^{R}$ as in Finite sums and finite products, by recursion. Let $ι : N \to R$ be the canonical natural of The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, so $ι (0) = 0$ and $ι (σ (n)) = ι (n) + 1$ . Then:

$ι$ is additive and multiplicative. $ι (1) = 1$ , and $ι (m + n) = ι (m) + ι (n)$ and $ι (m n) = ι (m) ι (n)$ for all $m, n \in N$ , the cases where a factor is $0$ included.
Additivity. $\sum_{k < n} (a_{k} + b_{k}) = \sum_{k < n} a_{k} + \sum_{k < n} b_{k}$ .
Constants. $\sum_{k < n} c = n \cdot c$ , the summand being the constant list.
Splitting. If $m \leq n$ and $d : = n - m$ , then $\sum_{k < n} a_{k} = \sum_{k < m} a_{k} + \sum_{j < d} a_{m + j}$ , and $\prod_{k < n} a_{k} = (\prod_{k < m} a_{k}) (\prod_{j < d} a_{m + j})$ .
Monotonicity. If $a_{k} \leq b_{k}$ for every $k < n$ then $\sum_{k < n} a_{k} \leq \sum_{k < n} b_{k}$ ; and $a_{j} \leq \sum_{k < n} a_{k}$ for every $j < n$ .
Products. $\prod_{k < n} (a_{k} b_{k}) = (\prod_{k < n} a_{k}) (\prod_{k < n} b_{k})$ ; and if $a_{k} \neq 0$ for every $k < n$ then $\prod_{k < n} a_{k} \neq 0$ .
The bridge into $R$ . $ι (\sum_{k < n}^{N} a_{k}) = \sum_{k < n}^{R} ι (a_{k})$ and $ι (\prod_{k < n}^{N} a_{k}) = \prod_{k < n}^{R} ι (a_{k})$ .
$ι$ is strictly increasing, hence injective. $m < n$ if and only if $ι (m) < ι (n)$ , and $m = n$ if and only if $ι (m) = ι (n)$ .

Clauses 6 and 7 together are the licence used everywhere below: an identity between natural numbers may be proved by proving the corresponding identity between their canonical naturals in $R$ , and conversely a real identity whose two sides are canonical naturals is an identity in $N$ .

Facts & Assumptions

Given: Lists $a, b : N \to N$ , a natural $c$ , naturals $m, n$ , and the ambient ordered field $R$ . Recall $σ (n) = n + 1$ and the truncated difference $n - m$ of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ .

[L1]

Induction: a property holding at $0$ and inherited by successors holds at every natural (The principle of mathematical induction).

[L2]

Recursion clauses in $N$ (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ): $\sum_{k < 0} a_{k} = 0$ , $\sum_{k < σ (n)} a_{k} = \sum_{k < n} a_{k} + a_{n}$ , $\prod_{k < 0} a_{k} = 1$ , $\prod_{k < σ (n)} a_{k} = (\prod_{k < n} a_{k}) \cdot a_{n}$ .

[L3]

Recursion clauses in $R$ (Finite sums and finite products, by recursion): $\sum_{k < 0}^{R} x_{k} = 0$ , $\sum_{k < σ (n)}^{R} x_{k} = \sum_{k < n}^{R} x_{k} + x_{n}$ , and likewise $\prod_{k < 0}^{R} x_{k} = 1$ , $\prod_{k < σ (n)}^{R} x_{k} = (\prod_{k < n}^{R} x_{k}) \cdot x_{n}$ .

[L4]

Arithmetic of $N$ : addition and multiplication are associative and commutative, $0 + n = n$ and $n + 0 = n$ , $1 \cdot n = n \cdot 1 = n$ and $0 \cdot n = n \cdot 0 = 0$ , multiplication distributes over addition, and $σ (a) \cdot n = a \cdot n + n$ (Addition is associative, Addition is commutative, Left identity for addition, Multiplication is associative, Multiplication is commutative, Zero and one under multiplication, Distributivity and the successor law for multiplication, Addition of natural numbers, Multiplication of natural numbers).

[L5]

Order of $N$ : $m \leq n$ means $m + j = n$ for some $j$ , that $j$ is unique, $m \leq n ⟺ m + k \leq n + k$ , and $m < n ⟺ σ (m) \leq n$ , so $n \neq 0$ is the same as $1 \leq n$ ; exactly one of $m < n$ , $m = n$ , $n < m$ holds (Order on the natural numbers, Addition is cancellative, Order is compatible with addition, Discreteness: $σ (n)$ is the immediate successor, Trichotomy of the order on $N$ ). Transitivity of $\leq$ follows from the definition and associativity: $m + j = n$ and $n + i = p$ give $m + (j + i) = p$ .

[L6]

The canonical natural (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field): $ι (0) = 0_{R}$ and $ι (σ (n)) = ι (n) + 1_{R}$ ; $ι (n)$ is also written $n \cdot 1_{R}$ .

[L7]

For $n \geq 1$ , with $n \cdot 1_{F}$ defined by $1 \cdot 1_{F} = 1_{F}$ and $(n + 1) \cdot 1_{F} = n \cdot 1_{F} + 1_{F}$ : $n \cdot 1_{F} > 0$ , and $(m + n) \cdot 1_{F} = m \cdot 1_{F} + n \cdot 1_{F}$ and $(m n) \cdot 1_{F} = (m \cdot 1_{F}) (n \cdot 1_{F})$ for all $m, n \geq 1$ (Canonical naturals are positive and strictly increasing). These identities are asserted for $m, n \geq 1$ only; the cases with a zero argument are checked separately below.

[L8]

In a field, $0 \cdot x = 0$ (Multiplication by zero: $0 \cdot a = 0$ ); and $R$ is an ordered field, so its addition and multiplication are associative and commutative with identities $0$ and $1$ , and its order is total and compatible with addition (Field, Ordered field).

[L9]

Cancellation in $N$ : $m \cdot k = n \cdot k$ with $k \neq 0$ implies $m = n$ (Cancellation for multiplication by a nonzero factor); and $σ (n) \neq 0$ , so $1 \neq 0$ (The von Neumann naturals form a Peano system).

Proof

technique · induction

1.1

Every clause is proved by induction on the upper index, using only the recursion clauses [L2], [L3] and the arithmetic [L4], [L8]; the inductions are written out one clause at a time.

given

1.2

The two notations agree: $ι (n) = n \cdot 1_{R}$ for every $n \geq 1$ . At $n = 1$ , $ι (1) = ι (σ (0)) = ι (0) + 1_{R} = 1_{R} = 1 \cdot 1_{R}$ ; and the successor clauses of the two recursions coincide, $ι (σ (n)) = ι (n) + 1_{R}$ and $(n + 1) \cdot 1_{R} = n \cdot 1_{R} + 1_{R}$ . So the two agree at every $n \geq 1$ by induction, and [L7] may be read as a statement about $ι$ .

L1L6L7

1.3

Clause 1 at $n = 0$ : both sides are the empty sum, $0 = 0 + 0$ .

baseL2L4

1.4

Clause 1, inductive hypothesis: assume $\sum_{k < n} (a_{k} + b_{k}) = \sum_{k < n} a_{k} + \sum_{k < n} b_{k}$ for a fixed $n$ and all lists $a, b$ .

1.5

Clause 2, by induction on $n$ . At $n = 0$ both sides are $0$ , since $0 \cdot c = 0$ . If $\sum_{k < n} c = n \cdot c$ , then $\sum_{k < σ (n)} c = \sum_{k < n} c + c = n \cdot c + c = σ (n) \cdot c$ , the last equality being the successor law $σ (a) \cdot n = a \cdot n + n$ of [L4].

L1L2L4

1.6

Clause 3, by induction on $d$ , with $m$ fixed and $n = m + d$ . At $d = 0$ we have $n = m$ and the second sum is empty, so the claim reads $\sum_{k < m} a_{k} = \sum_{k < m} a_{k} + 0$ . Assuming it at $d$ , and using $m + σ (d) = σ (m + d)$ , we get $\sum_{k < σ (n)} a_{k} = \sum_{k < n} a_{k} + a_{n} = (\sum_{k < m} a_{k} + \sum_{j < d} a_{m + j}) + a_{m + d} = \sum_{k < m} a_{k} + (\sum_{j < d} a_{m + j} + a_{m + d}) = \sum_{k < m} a_{k} + \sum_{j < σ (d)} a_{m + j}$ . The product form is the same argument with $+$ replaced by $\cdot$ and $0$ by $1$ .

L1L2L4L5

1.7

Clause 5, by induction on $n$ . At $n = 0$ both sides are $1 = 1 \cdot 1$ ; and $\prod_{k < σ (n)} (a_{k} b_{k}) = (\prod_{k < n} (a_{k} b_{k})) a_{n} b_{n} = (\prod_{k < n} a_{k}) (\prod_{k < n} b_{k}) a_{n} b_{n} = (\prod_{k < σ (n)} a_{k}) (\prod_{k < σ (n)} b_{k})$ by associativity and commutativity. For the second assertion, note first that a product of two nonzero naturals is nonzero: if $x y = 0$ with $y \neq 0$ , then $x y = 0 \cdot y$ , so $x = 0$ by [L9]. Now induct: $\prod_{k < 0} a_{k} = 1 \neq 0$ by [L9], and $\prod_{k < σ (n)} a_{k} = (\prod_{k < n} a_{k}) a_{n}$ is a product of two nonzero naturals.

L1L2L4L9

2.1

Clause 1, inductive step. Using [L2] twice and the associativity and commutativity of addition, $\sum_{k < σ (n)} (a_{k} + b_{k}) = \sum_{k < n} (a_{k} + b_{k}) + (a_{n} + b_{n}) = (\sum_{k < n} a_{k} + \sum_{k < n} b_{k}) + (a_{n} + b_{n}) = (\sum_{k < n} a_{k} + a_{n}) + (\sum_{k < n} b_{k} + b_{n}) = \sum_{k < σ (n)} a_{k} + \sum_{k < σ (n)} b_{k}$ , where the inductive hypothesis of step 1.4 was used at the second equality.

step 1.4L2L4

2.2

Clause 0. First $ι (1) = 1$ , computed in step 1.2. For $m, n \geq 1$ the two identities are [L7], read through step 1.2. If $n = 0$ then $ι (m + 0) = ι (m) = ι (m) + 0 = ι (m) + ι (0)$ , and $ι (m \cdot 0) = ι (0) = 0 = ι (m) \cdot 0 = ι (m) ι (0)$ by [L8]; the case $m = 0$ follows from these by the commutativity of addition and multiplication in $N$ and in $R$ . So both identities hold for all $m, n \in N$ .

step 1.2L4L7L8

2.3

Clause 4. Monotonicity is an induction: at $n = 0$ both sums are $0$ ; and if $\sum_{k < n} a_{k} \leq \sum_{k < n} b_{k}$ and $a_{n} \leq b_{n}$ , then $\sum_{k < n} a_{k} + a_{n} \leq \sum_{k < n} b_{k} + a_{n} \leq \sum_{k < n} b_{k} + b_{n}$ by [L5], so $\sum_{k < σ (n)} a_{k} \leq \sum_{k < σ (n)} b_{k}$ by transitivity. For the second assertion let $j < n$ , so $1 \leq n - j$ ; splitting at $j$ and then splitting the tail at $1$ , and using $\sum_{i < 1} a_{j + i} = 0 + a_{j} = a_{j}$ , gives $\sum_{k < n} a_{k} = (\sum_{k < j} a_{k} + a_{j}) + R$ for some $R \in N$ , and $a_{j} \leq (\sum_{k < j} a_{k} + a_{j}) + R$ because $a_{j}$ plus something equals it.

step 1.6L2L4L5

3.1

Clause 1 holds for every $n$ , by step 1.3 and step 2.1 together with induction.

step 1.3step 2.1L1

3.2

Clause 7. If $m < n$ put $d = n - m$ , so $m + d = n$ and $d \neq 0$ , hence $d \geq 1$ and $ι (d) > 0$ by [L7]; then $ι (n) = ι (m) + ι (d) > ι (m)$ by step 2.2. Conversely, if $ι (m) < ι (n)$ then $m = n$ and $n < m$ are both excluded, the first because the order of $R$ is irreflexive and the second by what was just proved, so $m < n$ by trichotomy in $N$ . The statement about equality follows by trichotomy on both sides.

step 2.2L5L7L8

3.3

Clause 6, by induction on $n$ . At $n = 0$ , $ι (\sum_{k < 0} a_{k}) = ι (0) = 0 = \sum_{k < 0}^{R} ι (a_{k})$ . Assuming the identity at $n$ , $ι (\sum_{k < σ (n)} a_{k}) = ι (\sum_{k < n} a_{k} + a_{n}) = ι (\sum_{k < n} a_{k}) + ι (a_{n}) = \sum_{k < n}^{R} ι (a_{k}) + ι (a_{n}) = \sum_{k < σ (n)}^{R} ι (a_{k})$ , the second equality by step 2.2. The product form is the same induction, starting from $ι (1) = 1$ and using multiplicativity.

step 2.2L1L2L3L6

4.1

Clause 0 is step 2.2, clause 1 is step 3.1, clause 2 is step 1.5, clause 3 is step 1.6, clause 4 is step 2.3, clause 5 is step 1.7, clause 6 is step 3.3 and clause 7 is step 3.2.

step 1.5step 1.6step 1.7step 2.3step 3.1step 3.2step 3.3discharge-induction∎

Remarks

Why the zero cases are done by hand. Canonical naturals are positive and strictly increasing states $(m + n) \cdot 1_{F} = m \cdot 1_{F} + n \cdot 1_{F}$ and $(m n) \cdot 1_{F} = (m \cdot 1_{F}) (n \cdot 1_{F})$ for $m, n \geq 1$ only, because the notation $n \cdot 1_{F}$ is introduced there by a recursion that starts at $1$ . Every count on this page can be $0$ , so the two one-line checks at $0$ in step 2.2 are not pedantry: without them clause 0 would be a citation to a statement that was not made.
The real-valued laws are the same list. Laws of finite sums and finite products proves additivity, scaling, splitting, monotonicity, telescoping and the product laws for sums of reals. The clauses above are their $N$ -valued counterparts, proved from the same recursion, and clause 6 is what ties the two lists together. Neither list contains a permutation-invariance clause; that is proved separately in the next item, and it is what the sum over a finite index set needs.
What clause 7 buys. Because $ι$ is injective, a proof may cross into $R$ , use subtraction or division there, and come back: if $ι (x) = ι (y)$ with $x, y \in N$ then $x = y$ . The binomial theorem below lives in $R$ for exactly this reason, while every coefficient in it is a count.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

A finite sum is unchanged by a permutation of its index range: $\sum_{k < n} a_{π (k)} = \sum_{k < n} a_{k}$ for every bijection $π : n \to n$

Statement

Let $n \in N$ and let $π : n \to n$ be a bijection (Injection, surjection, bijection). Then:

for every list $a : n \to R$ , $\sum_{k < n} a_{π (k)} = \sum_{k < n} a_{k}$ and $\prod_{k < n} a_{π (k)} = \prod_{k < n} a_{k}$ (Finite sums and finite products, by recursion);
for every list $a : n \to N$ , $\sum_{k < n} a_{π (k)} = \sum_{k < n} a_{k}$ and $\prod_{k < n} a_{π (k)} = \prod_{k < n} a_{k}$ (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ).

This is not in Laws of finite sums and finite products. That item proves additivity, scaling, splitting, monotonicity, telescoping and the product laws, and states no invariance clause; the same is true of the $N$ -valued list on this page. Permutation invariance is exactly what makes a sum over a finite set of indices well posed, which is the next item, so it is proved here first.

Facts & Assumptions

Given: A natural number $n$ , a bijection $π : n \to n$ , and a list $a$ of length $n$ . Throughout, $σ (n) = n \cup {n}$ , $n = {k : k < n}$ , and $*$ denotes any one of the four operations $(R, +)$ , $(R, \cdot)$ , $(N, +)$ , $(N, \cdot)$ , with $e$ the corresponding identity element $0$ , $1$ , $0$ , $1$ . Write $★_{k < n} c_{k}$ for the associated iterated operation, that is, for $\sum_{k < n} c_{k}$ in the two additive cases and $\prod_{k < n} c_{k}$ in the two multiplicative ones.

[L1]

Induction (The principle of mathematical induction).

[L2]

The four iterated operations obey the same two recursion clauses: $★_{k < 0} c_{k} = e$ and $★_{k < σ (n)} c_{k} = (★_{k < n} c_{k}) * c_{n}$ (Finite sums and finite products, by recursion, Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ).

[L3]

Each of the four operations is associative and commutative on its set and has $e$ as a two-sided identity (Field, Ordered field for $R$ ; Addition is associative, Addition is commutative, Multiplication is associative, Multiplication is commutative, Left identity for addition, Zero and one under multiplication for $N$ ). These three properties are the only facts about $*$ used below, which is why one argument proves all four clauses.

[L4]

Order and membership: $k < n ⟺ k \in n$ , $n = {k : k < n}$ , $k < σ (n) ⟺ k \leq n$ , $n \notin n$ , and $σ (n) ∖ {n} = n$ (On $N$ the order is membership: $m < n ⟺ m \in n$ , The natural numbers $N$ (von Neumann), Order on the natural numbers).

[L5]

Discreteness and successors: $m < n ⟺ σ (m) \leq n$ ; every nonzero natural is $σ (s)$ for a unique $s$ (Discreteness: $σ (n)$ is the immediate successor, Every nonzero natural number is a successor, The von Neumann naturals form a Peano system).

[L6]

Maps: a composite of bijections is a bijection; a bijection restricted to a subset of its domain is a bijection onto the image of that subset (Injection, surjection, bijection).

Proof

technique · induction

1.1

For $n \in N$ and $j \leq n$ define $d_{j}^{n} : n \to σ (n)$ by $d_{j}^{n} (k) = k$ for $k < j$ and $d_{j}^{n} (k) = σ (k)$ for $j \leq k < n$ ; this is the increasing enumeration of $σ (n) ∖ {j}$ . It is a bijection of $n$ onto $σ (n) ∖ {j}$ : its values lie in $σ (n)$ and avoid $j$ , since $k < j$ in the first clause and $σ (k) > k \geq j$ in the second; it is injective, being strictly increasing on each clause and satisfying $k < j \leq σ (k^{'})$ across them; and it is surjective, since $t \in σ (n)$ with $t < j$ has $t < n$ and $d_{j}^{n} (t) = t$ , while $t > j$ is nonzero, so $t = σ (s)$ with $j \leq s$ by [L5] and $s < n$ because $σ (s) \leq n$ , giving $d_{j}^{n} (s) = t$ .

L4L5L6construct

1.2

Claim $(A)$ at $n = 0$ : for a list $c$ of length $σ (0) = 1$ and the only admissible index $j = 0$ , both sides of $(A)$ read $c_{0}$ , since $★_{k < 1} c_{k} = e * c_{0} = c_{0}$ and $(★_{k < 0} c_{d_{0}^{0} (k)}) * c_{0} = e * c_{0} = c_{0}$ .

baseL2L3

1.3

Inductive hypothesis for $(A)$ : fix $n$ and assume that for every list $c$ of length $σ (n)$ and every $j \leq n$ one has $★_{k < σ (n)} c_{k} = (★_{k < n} c_{d_{j}^{n} (k)}) * c_{j}$ .

1.4

The main claim at $n = 0$ : the only bijection $0 \to 0$ is the empty map and both sides are the empty iterate $e$ .

2.1

Inductive step for $(A)$ . Let $c$ be a list of length $σ (σ (n))$ and let $j \leq σ (n)$ . If $j = σ (n)$ then $d_{j}^{σ (n)}$ is the identity of $σ (n)$ , so the right-hand side is $(★_{k < σ (n)} c_{k}) * c_{σ (n)}$ , which is the left-hand side by [L2]. If instead $j \leq n$ , apply the hypothesis of step 1.3 to the restriction of $c$ to $σ (n)$ to get $★_{k < σ (n)} c_{k} = (★_{k < n} c_{d_{j}^{n} (k)}) * c_{j}$ ; hence $★_{k < σ (σ (n))} c_{k} = ((★_{k < n} c_{d_{j}^{n} (k)}) * c_{j}) * c_{σ (n)} = ((★_{k < n} c_{d_{j}^{n} (k)}) * c_{σ (n)}) * c_{j}$ by [L3]. Finally $d_{j}^{σ (n)}$ agrees with $d_{j}^{n}$ on $n$ and sends $n$ to $σ (n)$ , because $j \leq n$ , so the inner bracket is $★_{k < σ (n)} c_{d_{j}^{σ (n)} (k)}$ by [L2], which is the right-hand side at $σ (n)$ .

step 1.3L2L3

3.1

Claim $(A)$ therefore holds for every $n$ : for every list $c$ of length $σ (n)$ and every $j \leq n$ , $★_{k < σ (n)} c_{k} = (★_{k < n} c_{d_{j}^{n} (k)}) * c_{j}$ . Informally, any single entry may be moved to the end without changing the value.

step 1.2step 2.1L1

4.1

Inductive step for the main claim. Assume it at $n$ , for every list of length $n$ and every bijection of $n$ . Let $π : σ (n) \to σ (n)$ be a bijection, let $a$ be a list of length $σ (n)$ , and put $j : = π^{- 1} (n) \leq n$ . Applying $(A)$ to the list $c_{k} : = a_{π (k)}$ at the index $j$ gives $★_{k < σ (n)} a_{π (k)} = (★_{k < n} a_{ρ (k)}) * a_{π (j)}$ with $ρ : = π \circ d_{j}^{n}$ and $a_{π (j)} = a_{n}$ . Now $ρ$ is a bijection of $n$ onto $n$ : $d_{j}^{n}$ is a bijection of $n$ onto $σ (n) ∖ {j}$ by step 1.1, and $π$ restricts to a bijection of $σ (n) ∖ {j}$ onto $σ (n) ∖ {n} = n$ . So the inductive hypothesis applies to $ρ$ and gives $★_{k < n} a_{ρ (k)} = ★_{k < n} a_{k}$ , whence $★_{k < σ (n)} a_{π (k)} = (★_{k < n} a_{k}) * a_{n} = ★_{k < σ (n)} a_{k}$ .

step 1.1step 3.1assume-hypL2L4L6

5.1

By induction the main claim holds for every $n \in N$ , every list of length $n$ and every bijection $π : n \to n$ .

step 1.4step 4.1L1

6.1

Since $*$ was any one of the four operations of the Given, and [L3] holds for each of them, step 5.1 is exactly clauses 1 and 2.

step 5.1L3discharge-induction∎

Remarks

Where the deletion map earns its keep. The usual textbook proof says "move the term $a_{n}$ to the end and delete it", and leaves the resulting map on the shorter index range unexamined. That map is $d_{j}^{n}$ composed with $π$ , and checking that it really is a bijection of $n$ onto $n$ is the only place where anything can go wrong; step 1.1 writes it down and verifies it in both directions.
One proof, four statements. Only associativity, commutativity, the identity and the two recursion clauses are used, so the argument is indifferent to which of the four operations is meant. The same observation is what later licenses the identical statement in an arbitrary monoid, where it belongs; nothing here needs that generality.
No choice is used. The index $j = π^{- 1} (n)$ is determined, not selected, because $π$ is a bijection.

DefinitionDefinition: AI-adaptedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form

Definition

Let $S$ be a finite set, $n : = ∣ S ∣$ (The cardinality $∣ A ∣$ of a finite set), and let $a : S \to R$ or $a : S \to N$ , written $a_{i}$ for $a (i)$ . Choose a bijection $φ : n \to S$ , which exists because $S \approx n$ (Equinumerous sets, $A \approx B$ and $A ⪯ B$ ), and set

$\sum_{i \in S} a_{i} : = \sum_{k < n} a_{φ (k)}, \prod_{i \in S} a_{i} : = \prod_{k < n} a_{φ (k)},$

the right-hand sides being the iterated operations of Finite sums and finite products, by recursion when the values are real and of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ when they are natural.

Independence of the enumeration, which is the content of the definition. Let $φ, ψ : n \to S$ be two bijections. Then $π : = φ^{- 1} \circ ψ$ is a bijection $n \to n$ (Injection, surjection, bijection), and $a_{ψ (k)} = a_{φ (π (k))}$ for every $k < n$ . Applying A finite sum is unchanged by a permutation of its index range: $\sum_{k < n} a_{π (k)} = \sum_{k < n} a_{k}$ for every bijection $π : n \to n$ to the list $c_{k} : = a_{φ (k)}$ gives

$\sum_{k < n} a_{ψ (k)} = \sum_{k < n} c_{π (k)} = \sum_{k < n} c_{k} = \sum_{k < n} a_{φ (k)},$

and identically for products. So the value does not depend on which bijection is used, and $\sum_{i \in S} a_{i}$ is a single well-determined element.

No choice principle is involved. The definition does not select an enumeration: it asserts that all enumerations give the same value, and that value is what the notation names. Only one bijection is ever produced at a time, from a set already known to be nonempty.

Three clauses, recorded here because the page uses them constantly.

(a) The bridge to the old notation. Taking $S = n$ and $φ = {i d}_{n}$ , which is legitimate since $∣ n ∣ = n$ , gives

$\sum_{i \in n} a_{i} = \sum_{k < n} a_{k}, \prod_{i \in n} a_{i} = \prod_{k < n} a_{k} .$

So the new notation extends the sum over an initial segment rather than competing with it, and every law proved for the latter is available for the former whenever the index set is a natural number.

(b) Reindexing along a bijection. If $h : T \to S$ is a bijection of finite sets, then $\sum_{j \in T} a_{h (j)} = \sum_{i \in S} a_{i}$ , and likewise for products. Indeed $∣ T ∣ = ∣ S ∣ = n$ by transport (The cardinality $∣ A ∣$ of a finite set), and if $φ : n \to S$ is a bijection then $h^{- 1} \circ φ : n \to T$ is one, so $\sum_{j \in T} a_{h (j)} = \sum_{k < n} a_{h (h^{- 1} (φ (k)))} = \sum_{k < n} a_{φ (k)} = \sum_{i \in S} a_{i}$ .

(c) The empty index set and a constant summand. $∣ \emptyset ∣ = 0$ , so $\sum_{i \in \emptyset} a_{i} = 0$ and $\prod_{i \in \emptyset} a_{i} = 1$ by the base clause of the recursion. And for a constant $c$ , clause (a) together with the constant clause of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ in $N$ , or clause 2 of Laws of finite sums and finite products in $R$ , gives

$\sum_{i \in S} c = ∣ S ∣ \cdot c (c \in N), \sum_{i \in S} c = ι (∣ S ∣) \cdot c (c \in R),$

the second with $ι$ written out because $∣ S ∣$ is a natural number and not an element of $R$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

Remarks

This is a different object from $\sum_{k < n} a_{k}$ , and the bridge is what keeps them one notion. The sum over an initial segment is indexed by a natural number and needs no well-definedness argument; the sum over a finite set is indexed by an arbitrary finite set and is well posed only because a finite sum is permutation invariant. Clause (a) is the statement that the second restricts to the first.
Splitting the index set — the identity $\sum_{i \in S \cup T} a_{i} = \sum_{i \in S} a_{i} + \sum_{i \in T} a_{i}$ for disjoint finite $S$ and $T$ , and its version for a finite partition — is not proved here but in The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, the next item, whose splice bijection is exactly what such a proof needs. Keeping the two together avoids building the same bijection twice.
Three notions of finite sum will exist in the library: over an initial segment (Finite sums and finite products, by recursion), over a finite index set (here), and in an arbitrary monoid (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity ↗, later in the reading order). Each is introduced with its bridge to the previous one, which is what stops them drifting apart.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition

Statement

Two blocks. If $A$ and $B$ are finite and disjoint, then $A \cup B$ is finite and $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ (The cardinality $∣ A ∣$ of a finite set).
A finite partition. If $I$ is a finite set and $(A_{i})_{i \in I}$ is a family of finite sets that are pairwise disjoint, then $⋃_{i \in I} A_{i}$ is finite and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , the sum being that of The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form.
Splitting a sum along a partition of its index set. Let $S$ be finite, let $J$ be finite, and let $(S_{j})_{j \in J}$ be pairwise disjoint subsets of $S$ with $⋃_{j \in J} S_{j} = S$ . Then for $a : S \to R$ or $a : S \to N$ , $\sum_{i \in S} a_{i} = \sum_{j \in J} (\sum_{i \in S_{j}} a_{i}), \prod_{i \in S} a_{i} = \prod_{j \in J} (\prod_{i \in S_{j}} a_{i}) .$ In particular $\sum_{i \in S \cup T} a_{i} = \sum_{i \in S} a_{i} + \sum_{i \in T} a_{i}$ for disjoint finite $S$ and $T$ .

Disjointness is a hypothesis and not a formality. It is spent at exactly one step, the injectivity of the splice map, and dropping it makes clause 1 false; the companion page carries that false statement with its smallest witness.

Facts & Assumptions

Given: Finite sets as in the statement, and the truncated difference and the two finite sums of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ . Throughout, $*$ denotes either $+$ or $\cdot$ on $R$ or on $N$ , $e$ the corresponding identity, and $★_{k < n} c_{k}$ the associated iterated operation; the four cases are proved by one argument, as in A finite sum is unchanged by a permutation of its index range: $\sum_{k < n} a_{π (k)} = \sum_{k < n} a_{k}$ for every bijection $π : n \to n$ .

[L1]

Induction (The principle of mathematical induction).

[L2]

Cardinality (The cardinality $∣ A ∣$ of a finite set): $∣ A ∣$ is the unique natural with $A \approx ∣ A ∣$ ; $∣ n ∣ = n$ ; $∣ \emptyset ∣ = 0$ ; a bijection transports finiteness and cardinality.

[L3]

Sums over a finite index set (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form): $\sum_{i \in S} a_{i} = \sum_{k < n} a_{φ (k)}$ for any bijection $φ : ∣ S ∣ \to S$ , the value being independent of $φ$ ; $\sum_{i \in n} a_{i} = \sum_{k < n} a_{k}$ ; reindexing along a bijection $T \to S$ leaves the value unchanged; and $\sum_{i \in \emptyset} a_{i} = e$ .

[L4]

Recursion clauses: $★_{k < 0} c_{k} = e$ and $★_{k < σ (n)} c_{k} = (★_{k < n} c_{k}) * c_{n}$ (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ , Finite sums and finite products, by recursion).

[L5]

Splitting at an index: for $p \leq N$ and $q = N - p$ , $★_{k < N} c_{k} = (★_{k < p} c_{k}) * (★_{j < q} c_{p + j})$ (clause 3 of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , clause 3 of Laws of finite sums and finite products).

[L6]

Order and addition in $N$ : $p \leq k$ gives a unique $j$ with $p + j = k$ ; $p + j < p + q ⟺ j < q$ ; addition is commutative; $σ (m) = m + 1$ (Order on the natural numbers, Addition is cancellative, Order is compatible with addition, Addition is commutative, Addition of natural numbers, On $N$ the order is membership: $m < n ⟺ m \in n$ ).

[L7]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ): composites and inverses of bijections are bijections, and an injective surjection is a bijection.

[L8]

A subset of a finite set is finite (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , clause 1).

Proof

technique · induction

1.1

The splice map. Let $A$ , $B$ be finite and disjoint, put $p : = ∣ A ∣$ , $q : = ∣ B ∣$ , and fix bijections $f : p \to A$ and $g : q \to B$ . Define $h : p + q \to A \cup B$ by $h (k) = f (k)$ when $k < p$ , and, when $p \leq k$ , by $h (k) = g (j)$ for the unique $j$ with $p + j = k$ ; that $j$ satisfies $j < q$ because $p + j = k < p + q$ . The map $h$ is well defined by [L6], it is surjective because every element of $A \cup B$ is some $f (k)$ or some $g (j)$ , and it is injective: two indices below $p$ are separated by the injectivity of $f$ , two indices at least $p$ by the injectivity of $g$ together with the uniqueness of $j$ , and an index below $p$ from one at least $p$ because $f (k) \in A$ , $g (j) \in B$ and $A \cap B = \emptyset$ . The last of these three cases is the only use of disjointness in the whole proof.

L6L7construct

1.2

Base cases of the two inductions below, at $m = 0$ . A family indexed by $0 = \emptyset$ has empty union, so $∣ ⋃_{k < 0} B_{k} ∣ = ∣ \emptyset ∣ = 0 = \sum_{k < 0} ∣ B_{k} ∣$ ; and a partition of $S$ indexed by $0$ forces $S = \emptyset$ , so both sides of clause 3 are $e$ .

baseL2L3L4

1.3

Inductive hypothesis for both inductions, at $m$ : for pairwise disjoint finite $B_{0}, \dots, B_{m - 1}$ the union $⋃_{k < m} B_{k}$ is finite with cardinality $\sum_{k < m} ∣ B_{k} ∣$ ; and for a partition of a finite set $S$ into pairwise disjoint $S_{0}, \dots, S_{m - 1}$ one has $★_{i \in S} a_{i} = ★_{k < m} (★_{i \in S_{k}} a_{i})$ .

2.1

Clause 1. By step 1.1 the map $h$ is a bijection $p + q \to A \cup B$ , so $A \cup B \approx p + q$ ; hence $A \cup B$ is finite and $∣ A \cup B ∣ = ∣ p + q ∣ = p + q = ∣ A ∣ + ∣ B ∣$ .

step 1.1L2L7

3.1

Clause 3 for two blocks. Let $S$ , $T$ be finite and disjoint and $a$ defined on $S \cup T$ . With $p = ∣ S ∣$ , $q = ∣ T ∣$ and the bijections $f, g, h$ of step 1.1 for the pair $S$ , $T$ , step 2.1 gives $∣ S \cup T ∣ = p + q$ , so $h$ may be used as the enumeration in [L3]. Then $★_{i \in S \cup T} a_{i} = ★_{k < p + q} a_{h (k)} = (★_{k < p} a_{h (k)}) * (★_{j < q} a_{h (p + j)}) = (★_{k < p} a_{f (k)}) * (★_{j < q} a_{g (j)}) = (★_{i \in S} a_{i}) * (★_{i \in T} a_{i})$ , using [L5] at the second equality.

step 1.1step 2.1L3L5

3.2

Inductive step for clause 2, in the case of an index set $σ (m)$ . Let $B_{0}, \dots, B_{m}$ be pairwise disjoint and finite. Then $⋃_{k < σ (m)} B_{k} = (⋃_{k < m} B_{k}) \cup B_{m}$ , and these two sets are disjoint because each $B_{k}$ with $k < m$ is disjoint from $B_{m}$ . By the hypothesis of step 1.3 the first is finite with cardinality $\sum_{k < m} ∣ B_{k} ∣$ , so clause 1 makes the union finite with cardinality $\sum_{k < m} ∣ B_{k} ∣ + ∣ B_{m} ∣ = \sum_{k < σ (m)} ∣ B_{k} ∣$ by [L4].

step 1.3step 2.1L4

4.1

Clause 2. By step 1.2, step 3.2 and induction, the statement holds for every family indexed by a natural number $m$ . For a general finite index set $I$ take a bijection $φ : m \to I$ with $m = ∣ I ∣$ ; then $⋃_{i \in I} A_{i} = ⋃_{k < m} A_{φ (k)}$ and $\sum_{i \in I} ∣ A_{i} ∣ = \sum_{k < m} ∣ A_{φ (k)} ∣$ by the definition of the sum over a finite index set, so the two statements coincide.

step 1.2step 3.2L1L3

5.1

Inductive step for clause 3, index set $σ (m)$ . Let $S$ be finite and partitioned into pairwise disjoint $S_{0}, \dots, S_{m}$ , and put $S^{'} : = ⋃_{k < m} S_{k}$ , which is finite by [L8] and disjoint from $S_{m}$ . The hypothesis of step 1.3 applies to the partition of $S^{'}$ into $S_{0}, \dots, S_{m - 1}$ , and step 3.1 applies to the disjoint pair $S^{'}$ , $S_{m}$ , giving $★_{i \in S} a_{i} = (★_{i \in S^{'}} a_{i}) * (★_{i \in S_{m}} a_{i}) = (★_{k < m} ★_{i \in S_{k}} a_{i}) * (★_{i \in S_{m}} a_{i}) = ★_{k < σ (m)} (★_{i \in S_{k}} a_{i})$ by [L4].

step 1.3step 3.1step 4.1L4L8

6.1

Clause 3. By step 1.2, step 5.1 and induction it holds for every index set that is a natural number, and the general finite $J$ follows by reindexing along a bijection $m \to J$ exactly as in step 4.1. The two-block form is step 3.1.

step 1.2step 3.1step 5.1L1L3

7.1

Clause 1 is step 2.1, clause 2 is step 4.1 and clause 3 is step 6.1; since $*$ was an arbitrary one of the four operations, both the sum and the product forms of clause 3 are proved.

step 2.1step 4.1step 6.1discharge-induction∎

Remarks

Why the splice map is built once. The same bijection $p + q \to A \cup B$ proves clause 1 and, used as an enumeration, proves the two-block case of clause 3. Building it twice, once for cardinalities and once for sums, would be two chances to get the index arithmetic wrong.
The subtraction in the splice is legitimate. Writing $h (k) = g (k - p)$ for $k \geq p$ means: the unique $j$ with $p + j = k$ , which exists by the definition of $\leq$ and is unique by cancellation. No negative number is formed anywhere.
Clause 3 is what the multinomial theorem needs. Its outer sum is indexed by the set of weak compositions of $n$ into $m$ parts, and the induction on $m$ partitions that index set by the value of the last part. Without clause 3 that step could not be taken.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$

Statement

If $A$ and $B$ are finite then $A \times B$ is finite and $∣ A \times B ∣ = ∣ A ∣ \cdot ∣ B ∣$ (The cardinality $∣ A ∣$ of a finite set).
Let $m \in N$ and let $A_{0}, \dots, A_{m - 1}$ be finite sets. Write $\prod_{i < m} A_{i} : = {f : f is a function with domain m and f (i) \in A_{i} for every i < m} .$ Then $\prod_{i < m} A_{i}$ is finite and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ , the right-hand product being the $N$ -valued one of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ .

At $m = 0$ clause 2 reads $∣ \prod_{i < 0} A_{i} ∣ = 1$ : there is exactly one function with domain $\emptyset$ , the empty function, and the empty product is $1$ . Both sides are computed, not stipulated.

Facts & Assumptions

Given: Finite sets $A$ , $B$ and a finite list $A_{0}, \dots, A_{m - 1}$ of finite sets. Recall $σ (m) = m \cup {m}$ and $m = {i : i < m}$ .

[L1]

Induction (The principle of mathematical induction).

[L2]

Cardinality (The cardinality $∣ A ∣$ of a finite set): $∣ A ∣$ is the unique natural with $A \approx ∣ A ∣$ ; $∣ n ∣ = n$ ; and a bijection transports finiteness and cardinality.

[L3]

The sum rule (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition): a family of pairwise disjoint finite sets indexed by a finite set has finite union, whose cardinality is the sum over that index set of the cardinalities.

[L4]

Sums over a finite index set (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form): $\sum_{i \in S} c = ∣ S ∣ \cdot c$ for a constant $c$ .

[L5]

Recursion clause for the $N$ -valued product (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ): $\prod_{i < 0} c_{i} = 1$ and $\prod_{i < σ (m)} c_{i} = (\prod_{i < m} c_{i}) \cdot c_{m}$ .

[L6]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ): a map with a two-sided inverse is a bijection, and composites of bijections are bijections.

[L7]

Arithmetic: multiplication of naturals is commutative (Multiplication is commutative, Multiplication of natural numbers); and $m = {i : i < m}$ , $σ (m) = m \cup {m}$ , $m \notin m$ (On $N$ the order is membership: $m < n ⟺ m \in n$ , The natural numbers $N$ (von Neumann)).

Proof

technique · induction

1.1

The slices. For $b \in B$ put $A_{b} : = A \times {b}$ . The map $a \mapsto (a, b)$ is a bijection of $A$ onto $A_{b}$ , with inverse the first projection, so $A_{b}$ is finite with $∣ A_{b} ∣ = ∣ A ∣$ ; and the family $(A_{b})_{b \in B}$ is pairwise disjoint, since an element of $A_{b}$ has second coordinate $b$ . Moreover $A \times B = ⋃_{b \in B} A_{b}$ .

L2L6construct

1.2

Base case of clause 2, at $m = 0$ . A function with domain $0 = \emptyset$ is the empty function and there is exactly one of them, so $\prod_{i < 0} A_{i} = {\emptyset}$ , which is finite with cardinality $1$ because $b \mapsto \emptyset$ is a bijection of $1 = {0}$ onto it; and $\prod_{i < 0} ∣ A_{i} ∣ = 1$ by [L5].

baseL2L5L6

1.3

Inductive hypothesis for clause 2: fix $m$ and assume that for every finite list $A_{0}, \dots, A_{m - 1}$ of finite sets the set $\prod_{i < m} A_{i}$ is finite with cardinality $\prod_{i < m} ∣ A_{i} ∣$ .

2.1

Clause 1. By step 1.1 and [L3], $A \times B$ is finite and $∣ A \times B ∣ = \sum_{b \in B} ∣ A_{b} ∣ = \sum_{b \in B} ∣ A ∣ = ∣ B ∣ \cdot ∣ A ∣ = ∣ A ∣ \cdot ∣ B ∣$ , using [L4] for the constant summand and commutativity for the last step.

step 1.1L3L4L7

3.1

Inductive step for clause 2. Let $A_{0}, \dots, A_{m}$ be finite. Define $Φ : \prod_{i < σ (m)} A_{i} \to (\prod_{i < m} A_{i}) \times A_{m}$ by $Φ (f) = (f ↾ m, f (m))$ , where $f ↾ m$ is the restriction of $f$ to $m$ . Its inverse is $(g, a) \mapsto g \cup {(m, a)}$ , a function with domain $σ (m) = m \cup {m}$ because $m \notin m$ ; the two composites are the identity, so $Φ$ is a bijection. By the hypothesis of step 1.3 and clause 1, the codomain is finite with cardinality $(\prod_{i < m} ∣ A_{i} ∣) \cdot ∣ A_{m} ∣ = \prod_{i < σ (m)} ∣ A_{i} ∣$ , and transport carries this to $\prod_{i < σ (m)} A_{i}$ .

step 1.3step 2.1L2L5L6L7

4.1

By step 1.2, step 3.1 and induction, clause 2 holds for every $m \in N$ .

step 1.2step 3.1L1

5.1

Clause 1 is step 2.1 and clause 2 is step 4.1.

step 2.1step 4.1discharge-induction∎

Remarks

No arithmetic is needed for clause 1. Slicing $A \times B$ over $B$ and applying the sum rule replaces the usual bijection $(p, q) \mapsto p ∣ B ∣ + q$ , which would have to be proved bijective by division with remainder. Division with remainder lives later in the reading order, so the slicing argument is not merely shorter here, it is the one available.
The empty cases are computed. With $A = \emptyset$ and $B$ arbitrary, clause 1 reads $∣ \emptyset ∣ = 0 \cdot ∣ B ∣ = 0$ , which is right because $\emptyset \times B = \emptyset$ . With $m = 0$ , clause 2 reads $1 = 1$ . Neither is a convention.
The infinite analogue of clause 1 fails in the shape a reader expects. A product of two infinite sets need not be strictly larger than either factor: $N \times N \approx N$ ( $N \times N \approx N$ ). The companion page records that as a false statement, with finiteness located as the hypothesis that fails.

DefinitionDefinition: AI-adaptedProof: AI-generatedverified 2026-08-02 (claude-opus-5)Open item page →

Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$

Definition

Let $m \in N$ . By the recursion theorem (The recursion theorem) applied to the set $N$ , the starting element $1$ and the function $f (x) = x \cdot m$ (Multiplication of natural numbers), there is a unique function $N \to N$ , written $n \mapsto m^{n}$ , with

$m^{0} = 1, m^{σ (n)} = m^{n} \cdot m (n \in N) .$

Both the base and the value are natural numbers, so $m^{n} \in N$ for all $m, n$ . In particular $m^{1} = m^{0} \cdot m = m$ and $m^{2} = m \cdot m$ .

Why a new item is needed. Integer powers $a^{m}$ defines $a^{n}$ for a real base $a$ , so its value is a real number. The counts on this page, $∣ A^{B} ∣$ and $∣ P (A) ∣$ among them, are natural numbers, and an identity between them has to be an identity in $N$ . The two operations are related by clause (d) below and by nothing weaker.

(a) $0^{0} = 1$ and $0^{n} = 0$ for $n \geq 1$ . The first is the base clause. For the second, $0^{σ (n)} = 0^{n} \cdot 0 = 0$ , the clause $x \cdot 0 = 0$ being definitional (Multiplication of natural numbers), and every $n \geq 1$ is a successor.

(b) $1^{n} = 1$ for every $n$ . Induction: $1^{0} = 1$ , and $1^{σ (n)} = 1^{n} \cdot 1 = 1^{n}$ (Zero and one under multiplication, The principle of mathematical induction).

(c) $m^{p + q} = m^{p} m^{q}$ and $(m p)^{q} = m^{q} p^{q}$ . Both by induction on $q$ , using associativity and commutativity of multiplication (Multiplication is associative, Multiplication is commutative). For the first, at $q = 0$ we have $m^{p + 0} = m^{p} = m^{p} \cdot 1 = m^{p} m^{0}$ , and $m^{p + σ (q)} = m^{σ (p + q)} = m^{p + q} \cdot m = (m^{p} m^{q}) \cdot m = m^{p} m^{σ (q)}$ , using $p + σ (q) = σ (p + q)$ (Addition of natural numbers). For the second, at $q = 0$ both sides are $1$ , and $(m p)^{σ (q)} = (m p)^{q} (m p) = m^{q} p^{q} m p = m^{σ (q)} p^{σ (q)}$ .

(d) The bridge into $R$ . With $ι : N \to R$ the canonical natural (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field) and $x^{n}$ the integer power of Integer powers $a^{m}$ ,

$ι (m^{n}) = ι (m)^{n} (m, n \in N) .$

Induction on $n$ : at $n = 0$ both sides are $1$ , since $ι (1) = 1$ ; and $ι (m^{σ (n)}) = ι (m^{n} \cdot m) = ι (m^{n}) ι (m) = ι (m)^{n} ι (m) = ι (m)^{σ (n)}$ , the second equality being the multiplicativity of $ι$ (clause 0 of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ ) and the last the recursion clause of Integer powers $a^{m}$ .

(e) $m^{n}$ is a constant product. $m^{n} = \prod_{k < n} m$ , the $N$ -valued product of the constant list (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ). Induction: at $n = 0$ both sides are $1$ , and $\prod_{k < σ (n)} m = (\prod_{k < n} m) \cdot m = m^{n} \cdot m = m^{σ (n)}$ .

Remarks

$0^{0} = 1$ , $0! = 1$ and the empty product are one convention, not three. The value $0^{0} = 1$ here is the base clause of the recursion above; by clause (e) it is the empty product of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ; and Integer powers $a^{m}$ adopts $a^{0} = 1$ for every real $a$ , $0$ included, so clause (d) is consistent at $m = n = 0$ . The reasons for the convention are set out in Integer powers $a^{m}$ and are not repeated here.
The laws are the same laws. Clause (c) is the $N$ -valued form of clause 1 of Laws of integer exponents, which states $a^{m + n} = a^{m} a^{n}$ , $(a^{m})^{n} = a^{m n}$ and $(a b)^{n} = a^{n} b^{n}$ for a base in a field. Only the two identities actually used on this page are proved above; the third is available in $R$ through clause (d) whenever it is wanted.
The exponent stays a natural number. Following the convention of Finite sums and finite products, by recursion, the identification of a natural with its canonical natural is deliberately not made in an exponent: in $m^{n}$ and in $ι (m)^{n}$ the exponent $n$ is a natural number, never a real.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$

Statement

Let $A$ and $B$ be finite sets and write

$A^{B} : = {f : f is a function B \to A} .$

Then $A^{B}$ is finite and $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ , the power being the $N$ -valued exponentiation of Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ .

Both degenerate cases are covered and neither is a stipulation. If $B = \emptyset$ there is exactly one function $B \to A$ , the empty function, so $∣ A^{\emptyset} ∣ = 1 = ∣ A ∣^{0}$ even when $A = \emptyset$ . If $A = \emptyset$ and $B \neq \emptyset$ there is no function at all, so $∣ A^{B} ∣ = 0 = 0^{∣ B ∣}$ with $∣ B ∣ \geq 1$ .

Facts & Assumptions

Given: Finite sets $A$ and $B$ , and $n : = ∣ B ∣$ . Here $A^{B}$ is the SET of functions $B \to A$ ; it carries no further structure.

[L1]

Induction (The principle of mathematical induction).

[L2]

Cardinality (The cardinality $∣ A ∣$ of a finite set): $∣ A ∣$ is the unique natural with $A \approx ∣ A ∣$ ; $∣ n ∣ = n$ ; $∣ A ∣ = 0$ exactly when $A = \emptyset$ ; and a bijection transports finiteness and cardinality.

[L3]

The sum rule for two disjoint blocks: $∣ S \cup T ∣ = ∣ S ∣ + ∣ T ∣$ (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, clause 1).

[L4]

The product rule: $∣ X \times Y ∣ = ∣ X ∣ \cdot ∣ Y ∣$ for finite $X$ , $Y$ (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ , clause 1).

[L5]

Powers (Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ ): $m^{0} = 1$ and $m^{σ (n)} = m^{n} \cdot m$ .

[L6]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ): a map with a two-sided inverse is a bijection.

[L7]

A subset of a finite set is finite (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , clause 1); cancellation in $N$ : $x + 1 = y + 1$ implies $x = y$ (Addition is cancellative); and $σ (n) = n + 1$ , $n = {i : i < n}$ (The natural numbers $N$ (von Neumann), On $N$ the order is membership: $m < n ⟺ m \in n$ ).

Proof

technique · induction

1.1

Base case $∣ B ∣ = 0$ . Then $B = \emptyset$ by [L2], and a function $\emptyset \to A$ is the empty function, of which there is exactly one whatever $A$ is; so $A^{B} = {\emptyset}$ , which is finite with cardinality $1$ because $0 \mapsto \emptyset$ is a bijection of $1 = {0}$ onto it. And $∣ A ∣^{0} = 1$ by [L5].

baseL2L5L6

1.2

Inductive hypothesis: fix $n \in N$ and assume that for every finite $A$ and every finite $B^{'}$ with $∣ B^{'} ∣ = n$ the set $A^{B^{'}}$ is finite with $∣ A^{B^{'}} ∣ = ∣ A ∣^{n}$ .

2.1

Inductive step. Let $∣ B ∣ = σ (n)$ . Then $B \neq \emptyset$ by [L2], so fix $b \in B$ and put $B^{'} : = B ∖ {b}$ , which is finite by [L7]. Since $B = B^{'} \cup {b}$ with $B^{'} \cap {b} = \emptyset$ and $∣ {b} ∣ = 1$ , [L3] gives $σ (n) = ∣ B^{'} ∣ + 1$ , hence $∣ B^{'} ∣ = n$ by cancellation. Define $Ψ : A^{B} \to A^{B^{'}} \times A$ by $Ψ (f) = (f ↾ B^{'}, f (b))$ ; its inverse is $(g, a) \mapsto g \cup {(b, a)}$ , which is a function on $B^{'} \cup {b} = B$ because $b \notin B^{'}$ , and the two composites are the identity, so $Ψ$ is a bijection. By the hypothesis of step 1.2 and by [L4] the codomain is finite with cardinality $∣ A ∣^{n} \cdot ∣ A ∣ = ∣ A ∣^{σ (n)}$ , and transport carries this to $A^{B}$ .

step 1.2L2L3L4L5L6L7construct

3.1

By induction on $∣ B ∣$ the statement holds for every pair of finite sets $A$ , $B$ .

step 1.1step 2.1L1

4.1

The two degenerate readings are instances of it: $B = \emptyset$ gives $1 = ∣ A ∣^{0}$ by step 1.1, valid for $A = \emptyset$ as well; and $A = \emptyset$ with $∣ B ∣ \geq 1$ gives $∣ A^{B} ∣ = 0^{∣ B ∣} = 0$ , which is right because a function $B \to \emptyset$ would have to supply a value in $\emptyset$ for some element of $B$ .

step 1.1step 3.1L2L5discharge-induction∎

Remarks

Where the choice of $b$ sits. A single element is taken from a single nonempty set, which is an ordinary existential instantiation and not a choice principle. Nothing in the argument selects a point of every member of a family.
$A^{B}$ here is a bare set. The same set carries a vector space structure over a field in The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = {0, 1, \dots, n - 1}$ ↗, much later in the reading order; that structure is not used, and this theorem is a count and nothing more.
The exponent notation is not an accident. $∣ A ∣^{∣ B ∣}$ counts the functions $B \to A$ , and $∣ A ∣^{n}$ is by clause (e) of Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ the product of $n$ copies of $∣ A ∣$ : one factor for each element of the domain, which is exactly what the inductive step does one point at a time.

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

$∣ P (A) ∣ = 2^{∣ A ∣}$ for finite $A$

Statement

Let $A$ be a finite set and $n : = ∣ A ∣$ . Then the power set $P (A)$ is finite and

$∣ P (A) ∣ = 2^{n},$

the power being the $N$ -valued exponentiation of Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ . Moreover $n < 2^{n}$ .

The last inequality is the quantitative form, for finite $A$ , of Cantor's theorem $A ≺ P (A)$ (Cantor's theorem: $A ≺ P (A)$ ), which holds for every set whatsoever. The two statements are consistent and the proof below derives the inequality from Cantor's theorem rather than leaving them side by side.

Facts & Assumptions

Given: A finite set $A$ with $n : = ∣ A ∣$ , and $2 = {0, 1}$ as a von Neumann natural (The natural numbers $N$ (von Neumann)). Write $2^{A}$ for the set of functions $A \to 2$ .

[L1]

$∣ X^{Y} ∣ = ∣ X ∣^{∣ Y ∣}$ for finite $X$ , $Y$ , and $X^{Y}$ is finite (The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ ).

[L2]

Cardinality (The cardinality $∣ A ∣$ of a finite set): $∣ m ∣ = m$ for a natural $m$ ; a bijection transports finiteness and cardinality; and for finite $X$ , $Y$ one has $∣ X ∣ = ∣ Y ∣$ if and only if $X \approx Y$ .

[L3]

Cantor's theorem: $A ≺ P (A)$ , that is, there is an injection $A \to P (A)$ and no bijection (Cantor's theorem: $A ≺ P (A)$ , Equinumerous sets, $A \approx B$ and $A ⪯ B$ ).

[L4]

Pigeonhole, claim 2: if $q < p$ then there is no injection $p \to q$ (The pigeonhole principle on $N$ ).

[L5]

Trichotomy: exactly one of $p < q$ , $p = q$ , $q < p$ holds (Trichotomy of the order on $N$ , Order on the natural numbers).

[L6]

Maps (Injection, surjection, bijection): a map with a two-sided inverse is a bijection; a composite of injections is an injection; and $f^{- 1} [T] = {x : f (x) \in T}$ .

Proof

technique · direct

1.1

The characteristic function. For $S \subseteq A$ define $χ_{S} : A \to 2$ by $χ_{S} (x) = 1$ when $x \in S$ and $χ_{S} (x) = 0$ otherwise, and let $X : P (A) \to 2^{A}$ be $S \mapsto χ_{S}$ . Let $Y : 2^{A} \to P (A)$ be $f \mapsto f^{- 1} [{1}]$ . Both composites are the identity: $χ_{S}^{- 1} [{1}] = {x \in A : χ_{S} (x) = 1} = S$ ; and for $f : A \to 2$ and $x \in A$ the value $f (x)$ is $0$ or $1$ , so $χ_{f^{- 1} [{1}]} (x) = 1$ exactly when $f (x) = 1$ and $= 0$ otherwise, that is $χ_{f^{- 1} [{1}]} = f$ . Hence $X$ is a bijection and $P (A) \approx 2^{A}$ .

L6construct

2.1

Therefore $P (A)$ is finite and $∣ P (A) ∣ = ∣ 2^{A} ∣ = ∣ 2 ∣^{∣ A ∣} = 2^{n}$ , using [L1] and $∣ 2 ∣ = 2$ from [L2].

step 1.1L1L2

3.1

The inequality. By [L3] there is an injection $A \to P (A)$ ; composing with bijections $n \to A$ and $P (A) \to 2^{n}$ , which exist by [L2] and step 2.1, gives an injection $n \to 2^{n}$ . So $2^{n} < n$ is impossible by [L4], and $n \leq 2^{n}$ by [L5]. Also $n \neq 2^{n}$ : otherwise $∣ A ∣ = ∣ P (A) ∣$ , hence $A \approx P (A)$ by [L2], contradicting [L3].

step 2.1L2L3L4L5L6

4.1

The two assertions are step 2.1 and step 3.1, so $∣ P (A) ∣ = 2^{n}$ and $n < 2^{n}$ .

step 2.1step 3.1∎

Remarks

The finiteness of $P (A)$ is part of the statement, and it is what makes $[A]^{k}$ finite in the next definition: a set of $k$ -element subsets is a subset of $P (A)$ .
Cantor's theorem is not weakened here. $A ≺ P (A)$ holds for every set, finite or infinite, and needs no counting; what the finite case adds is the value of the gap, $2^{n}$ against $n$ . The inequality above is deduced from Cantor's theorem, so no independent argument can disagree with it.

DefinitionDefinition: AI-adaptedProof: AI-generatedverified 2026-08-02 (claude-opus-5)Open item page →

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$

Definition

The factorial. By the recursion theorem (The recursion theorem) applied to the set $N \times N$ , the starting element $(0, 1)$ and the function $f (k, v) = (σ (k), v \cdot σ (k))$ , and by the same induction on the first coordinate as in Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ , there is a unique $F : N \to N$ with

$F (0) = 1, F (σ (n)) = F (n) \cdot σ (n) (n \in N) .$

We write $n! : = F (n)$ . Thus $0! = 1$ , $1! = 0! \cdot 1 = 1$ , $2! = 1! \cdot 2 = 2$ , $3! = 6$ , $4! = 24$ , $5! = 120$ , $6! = 720$ .

$0! = 1$ is the base clause of this recursion, not a convention imported from elsewhere. Nothing about empty products is presupposed; the agreement with the empty product is proved below, in clause (a), rather than assumed.

Truncated difference. Throughout, $n - k$ is the operation fixed in Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ : the unique $j$ with $k + j = n$ when $k \leq n$ , and $0$ when $n < k$ .

The falling factorial. For $n \in N$ define $n^{\underline{k}}$ by recursion on $k$ , by the recursion theorem applied to $N \times N$ with starting element $(0, 1)$ and $f (k, v) = (σ (k), v \cdot (n - k))$ :

$n^{\underline{0}} = 1, n^{\underline{σ (k)}} = n^{\underline{k}} \cdot (n - k) .$

So $n^{\underline{1}} = 1 \cdot (n - 0) = n$ and $n^{\underline{2}} = n (n - 1)$ , and for $k \leq n$ the value is the product $n (n - 1) \dots (n - k + 1)$ of the $k$ topmost factors.

Four facts, proved here because the page uses each of them.

(a) The factorial is the product of the first $n$ positive naturals. $n! = \prod_{j < n} σ (j) = \prod_{j < n} (j + 1)$ , the $N$ -valued product of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ . Induction (The principle of mathematical induction): at $n = 0$ both sides are $1$ , the empty product and the base clause agreeing; and $\prod_{j < σ (n)} σ (j) = (\prod_{j < n} σ (j)) \cdot σ (n) = n! \cdot σ (n) = σ (n)!$ . So the empty-product reading and the base-clause reading are the same reading, and neither was assumed.

(b) $n! \neq 0$ , and $ι (n!) = \prod_{j < n}^{R} ι (j + 1)$ . For the first, $0! = 1 \neq 0$ (The von Neumann naturals form a Peano system) and $σ (n)! = n! \cdot σ (n)$ is a product of two nonzero naturals, which is nonzero: if $x y = 0$ with $y \neq 0$ then $x y = 0 \cdot y$ (Zero and one under multiplication) and cancellation gives $x = 0$ (Cancellation for multiplication by a nonzero factor). So $n! \neq 0$ for every $n$ by induction. For the second, apply the bridge clause 6 of that lemma to clause (a) above. This is what makes the factorial of this page and the real-valued product $\prod_{j < n} (j + 1)$ used elsewhere in the library one object seen twice, rather than two unrelated notions.

(c) $n^{\underline{k}} \cdot (n - k)! = n!$ for $k \leq n$ . Induction on $k$ , for all $n$ at once. At $k = 0$ this reads $1 \cdot n! = n!$ . Assume it at $k$ and let $σ (k) \leq n$ ; then $k \leq n$ , and writing $d : = n - k$ we have $k + d = n$ and $d \neq 0$ , since $k + 0 = k \neq n$ ; so $d = σ (e)$ for a unique $e$ (Every nonzero natural number is a successor), and $σ (k) + e = n$ , that is $e = n - σ (k)$ (Addition is cancellative). Therefore $n^{\underline{σ (k)}} \cdot (n - σ (k))! = n^{\underline{k}} \cdot (n - k) \cdot e! = n^{\underline{k}} \cdot (e! \cdot σ (e)) = n^{\underline{k}} \cdot σ (e)! = n^{\underline{k}} \cdot (n - k)! = n!$ , using commutativity and associativity of multiplication (Multiplication is associative, Multiplication is commutative) and the recursion clause for the factorial.

(d) Boundary values. $n^{\underline{0}} = 1$ for every $n$ , by the base clause; $n^{\underline{n}} = n!$ , since clause (c) at $k = n$ gives $n^{\underline{n}} \cdot 0! = n!$ and $0! = 1$ ; and $n^{\underline{k}} = 0$ whenever $k > n$ . For the last, $n - n = 0$ gives $n^{\underline{σ (n)}} = n^{\underline{n}} \cdot 0 = 0$ , the clause $x \cdot 0 = 0$ being definitional (Multiplication of natural numbers), and if $n^{\underline{k}} = 0$ then $n^{\underline{σ (k)}} = 0$ as well, so $n^{\underline{k}} = 0$ for every $k \geq σ (n)$ by induction.

Remarks

Why $0! = 1$ is not imported. The empty-product convention of an arbitrary monoid is fixed in The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity ↗, which comes later in the reading order, so citing it here would be a dependency pointing the wrong way. Taking $0! = 1$ as the base clause of the factorial's own recursion costs nothing and owes nothing, and clause (a) then records the agreement.
The library's other factorial. For every real $x$ , $x^{k} / k! \to 0$ ↗, later in the reading order, works with a real-valued factorial defined as the product $\prod_{j < n} (j + 1)$ in $R$ . Clause (b) says that this is exactly $ι (n!)$ , so the two agree and no second notion has been created. That pointer is orientation only.
Check every clause at $k = 0$ and at $k = n$ . The falling factorial is defined by two regimes, one for $k \leq n$ and one beyond, and the recursion above covers both because the truncated difference is $0$ past the end. The two values that get used constantly are $n^{\underline{0}} = 1$ and $n^{\underline{n}} = n!$ , and both are clause (d).

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The number of injections from a $k$ -element set into an $n$ -element set is $n^{\underline{k}}$

Statement

Let $A$ and $B$ be finite sets, $n : = ∣ A ∣$ and $k : = ∣ B ∣$ , and write

$Inj (B, A) : = {f : B \to A : f is injective} .$

Then $Inj (B, A)$ is finite and $∣ Inj (B, A) ∣ = n^{\underline{k}}$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

The two boundary readings are part of the statement. At $k = 0$ there is exactly one injection, the empty function, and $n^{\underline{0}} = 1$ . For $k > n$ there is none, and $n^{\underline{k}} = 0$ .

Facts & Assumptions

Given: Finite sets $A$ , $B$ with $n = ∣ A ∣$ and $k = ∣ B ∣$ . The truncated difference $n - k$ is that of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ .

[L1]

Induction (The principle of mathematical induction).

[L2]

Cardinality (The cardinality $∣ A ∣$ of a finite set): $∣ X ∣ = 0$ exactly when $X = \emptyset$ ; a bijection transports finiteness and cardinality; $∣ m ∣ = m$ .

[L3]

The falling factorial (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ): $n^{\underline{0}} = 1$ , $n^{\underline{σ (k)}} = n^{\underline{k}} \cdot (n - k)$ , and $n^{\underline{k}} = 0$ for $k > n$ .

[L4]

$X^{Y}$ is finite for finite $X$ , $Y$ (The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ ), and a subset of a finite set is finite, with $∣ B^{'} ∣ \leq ∣ B ∣$ (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , clauses 1 and 2).

[L5]

The sum rule (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition): $∣ S \cup T ∣ = ∣ S ∣ + ∣ T ∣$ for disjoint finite $S$ , $T$ ; and a pairwise disjoint family of finite sets indexed by a finite set has finite union with cardinality the sum of the cardinalities. Together with $\sum_{i \in S} c = ∣ S ∣ \cdot c$ (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form).

[L6]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ): a map with a two-sided inverse is a bijection; the restriction of an injection is an injection; an injection is a bijection onto its image.

[L7]

Order and cancellation in $N$ : $x + 1 = y + 1$ implies $x = y$ ; if $k + t = n$ then $t = n - k$ ; trichotomy (Addition is cancellative, Order on the natural numbers, Trichotomy of the order on $N$ ).

Proof

technique · induction

1.1

Base case $k = 0$ . Then $B = \emptyset$ , and the only function $\emptyset \to A$ is the empty function, which is injective because injectivity is a condition on pairs of points of the domain and there are none. So $Inj (B, A) = {\emptyset}$ has cardinality $1 = n^{\underline{0}}$ .

baseL2L3L6

1.2

Inductive hypothesis: fix $k$ and assume that for all finite $A$ , $B^{'}$ with $∣ A ∣ = n$ and $∣ B^{'} ∣ = k$ the set $Inj (B^{'}, A)$ is finite with cardinality $n^{\underline{k}}$ .

1.3

Setting up the inductive step. Let $∣ B ∣ = σ (k)$ , so $B \neq \emptyset$ ; fix $b \in B$ and put $B^{'} : = B ∖ {b}$ , which is finite with $∣ B^{'} ∣ = k$ by [L4], [L5] and cancellation, exactly as in the count of $A^{B}$ . Put $T : = {(g, a) : g \in Inj (B^{'}, A), a \in A ∖ g [B^{'}]}$ and define $Φ : Inj (B, A) \to T$ by $Φ (f) = (f ↾ B^{'}, f (b))$ ; this lands in $T$ because $f ↾ B^{'}$ is injective and $f (b) \neq f (x)$ for $x \in B^{'}$ , so $f (b) \notin f [B^{'}]$ . The map $(g, a) \mapsto g \cup {(b, a)}$ is a two-sided inverse: the extension is injective precisely because $a \notin g [B^{'}]$ . So $Φ$ is a bijection. Finally $Inj (B^{'}, A) \subseteq A^{B^{'}}$ is finite by [L4].

L4L5L6L7construct

2.1

The case $k > n$ . Then $n^{\underline{k}} = 0$ by [L3], so the hypothesis of step 1.2 gives $∣ Inj (B^{'}, A) ∣ = 0$ , that is $Inj (B^{'}, A) = \emptyset$ ; hence $T = \emptyset$ and $Inj (B, A) = \emptyset$ by step 1.3, so its cardinality is $0$ . And $σ (k) > n$ as well, so $n^{\underline{σ (k)}} = 0$ by [L3]. Both sides are $0$ .

step 1.2step 1.3L2L3

2.2

The case $k \leq n$ . For each $g \in Inj (B^{'}, A)$ the image $g [B^{'}]$ is a subset of $A$ with $∣ g [B^{'}] ∣ = ∣ B^{'} ∣ = k$ , since $g$ is a bijection onto its image; and $A$ is the disjoint union of $g [B^{'}]$ and $A ∖ g [B^{'}]$ , so $n = k + ∣ A ∖ g [B^{'}] ∣$ by [L5] and therefore $∣ A ∖ g [B^{'}] ∣ = n - k$ by [L7]. Now $T$ is the union of the pairwise disjoint sets ${g} \times (A ∖ g [B^{'}])$ indexed by $g \in Inj (B^{'}, A)$ , each of cardinality $n - k$ because $a \mapsto (g, a)$ is a bijection; so [L5] gives $∣ T ∣ = \sum_{g} (n - k) = ∣ Inj (B^{'}, A) ∣ \cdot (n - k) = n^{\underline{k}} \cdot (n - k) = n^{\underline{σ (k)}}$ , using the hypothesis of step 1.2 and [L3]. With step 1.3 this is $∣ Inj (B, A) ∣$ .

step 1.2step 1.3L2L3L5L6L7

3.1

The two cases are exhaustive by trichotomy, so the statement holds at $σ (k)$ whenever it holds at $k$ ; with step 1.1 it holds for every $k$ , and the two boundary readings are step 1.1 and step 2.1.

step 1.1step 2.1step 2.2L1L7discharge-induction∎

Remarks

The two regimes of the falling factorial are the two cases of the proof. $n^{\underline{k}}$ was defined by a single recursion whose factor $n - k$ is truncated at $0$ , and step 2.1 is exactly the regime where that truncation bites. Writing the cases out is what keeps the theorem true past $k = n$ instead of only up to it.
Pigeonhole is not needed. That no injection exists when $k > n$ is here a consequence of the induction rather than a citation of The pigeonhole principle on $N$ ; the two agree, and the lemma remains what makes $∣ \cdot ∣$ well posed in the first place.
The count is of a set of functions. $Inj (B, A)$ is a subset of $A^{B}$ , so its finiteness comes from The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ and A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ rather than being assumed.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

A finite set $A$ with $∣ A ∣ = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality

Statement

Let $A$ be a finite set with $n : = ∣ A ∣$ and write

$Bij (A) : = {f : A \to A : f is a bijection} .$

Then $Bij (A)$ is finite and $∣ Bij (A) ∣ = n!$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

More generally, for finite sets $X$ and $Y$ write $Bij (X, Y)$ for the set of bijections $X \to Y$ . If $∣ X ∣ = ∣ Y ∣ = n$ then $Bij (X, Y)$ is finite with $n!$ elements, and if $∣ X ∣ \neq ∣ Y ∣$ then $Bij (X, Y) = \emptyset$ .

Facts & Assumptions

Given: Finite sets $A$ , $X$ , $Y$ , with $n = ∣ A ∣$ .

[L1]

$∣ Inj (B, A) ∣ = ∣ A ∣^{\underline{∣ B ∣}}$ , and $Inj (B, A)$ is finite (The number of injections from a $k$ -element set into an $n$ -element set is $n^{\underline{k}}$ ).

[L2]

Every injection of a finite set into itself is a bijection (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , clause 4).

[L3]

$n^{\underline{n}} = n!$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ , clause (d)).

[L4]

Cardinality (The cardinality $∣ A ∣$ of a finite set): a bijection transports finiteness and cardinality, and for finite $X$ , $Y$ one has $∣ X ∣ = ∣ Y ∣$ if and only if $X \approx Y$ .

[L5]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ): composites and inverses of bijections are bijections, and every bijection is an injection.

Proof

technique · direct

1.1

The two sets coincide: $Bij (A) = Inj (A, A)$ . Every bijection is an injection, and by [L2] every injection $A \to A$ is a bijection, $A$ being finite.

L2L5

2.1

Hence $Bij (A)$ is finite with $∣ Bij (A) ∣ = ∣ Inj (A, A) ∣ = n^{\underline{n}} = n!$ , by [L1] with $B = A$ and by [L3].

step 1.1L1L3

3.1

The two-set form. Suppose $∣ X ∣ = ∣ Y ∣ = n$ . Then $X \approx Y$ by [L4], so fix a bijection $u : Y \to X$ . The map $g \mapsto u \circ g$ sends $Bij (X, Y)$ into $Bij (X, X) = Bij (X)$ and has the two-sided inverse $h \mapsto u^{- 1} \circ h$ , so it is a bijection; hence $Bij (X, Y)$ is finite with $∣ Bij (X, Y) ∣ = ∣ Bij (X) ∣ = n!$ by step 2.1 and [L4]. If instead $∣ X ∣ \neq ∣ Y ∣$ then $X \approx̸ Y$ by [L4], so no bijection $X \to Y$ exists at all.

step 2.1L4L5

4.1

The first assertion is step 2.1 and the second is step 3.1.

step 2.1step 3.1∎

Remarks

No group vocabulary is used or needed. $Bij (A)$ is written here as a set of bijections. Composition makes it a group, and that structure, together with the name symmetric group, is introduced in The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition ↗ later in the reading order; the pointer is orientation only and nothing above rests on it. The count $n!$ proved here is what a later page needs in order to say that the symmetric group on $n$ letters has $n!$ elements.
Why this is on the main page and not among the examples. Later pages consume this count, and an examples page is a leaf that nothing else may depend on.
The two-set form costs one line and is used immediately. The closed formula for $(\binom{n}{k})$ counts the bijections between an initial segment and an arbitrary $k$ -element subset, which is exactly $Bij (X, Y)$ with $X \neq Y$ .

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$

Definition

For a finite set $A$ and $k \in N$ put

$[A]^{k} : = {S \subseteq A : ∣ S ∣ = k},$

the set of $k$ -element subsets of $A$ . Every $S \subseteq A$ is finite (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ), so the condition $∣ S ∣ = k$ makes sense for every subset.

$[A]^{k}$ is finite. It is a subset of $P (A)$ , which is finite by $∣ P (A) ∣ = 2^{∣ A ∣}$ for finite $A$ , so A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ applies.

$∣ [A]^{k} ∣$ depends only on $∣ A ∣$ . Let $h : A \to A^{'}$ be a bijection of finite sets. The direct image map $S \mapsto h [S]$ carries $[A]^{k}$ into $[A^{'}]^{k}$ , because $h$ restricted to $S$ is a bijection of $S$ onto $h [S]$ and so $∣ h [S] ∣ = ∣ S ∣ = k$ by the transport clause of The cardinality $∣ A ∣$ of a finite set; the map $T \mapsto h^{- 1} [T]$ is its two-sided inverse, since $h^{- 1} [h [S]] = S$ and $h [h^{- 1} [T]] = T$ for a bijection $h$ . So $[A]^{k} \approx [A^{'}]^{k}$ and the two have the same cardinality.

Definition. For $n, k \in N$ set

$(\binom{n}{k}) : = ∣ [n]^{k} ∣ \in N,$

the binomial coefficient. By the previous paragraph and $∣ n ∣ = n$ ,

$∣ [A]^{k} ∣ = (\binom{∣ A ∣}{k}) for every finite A .$

$(\binom{n}{k})$ is a count, so it is a natural number by construction. It is not defined as $n! / (k! (n - k)!)$ : that expression involves a division, hence lives in $R$ , and the assertion that its value is a natural number is a theorem, proved in $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ . Defining the coefficient as a count makes integrality free and leaves the closed formula something to prove.

Boundary values, read off the definition and not stipulated.

$(\binom{n}{0}) = 1$ for every $n$ , including $n = 0$ : the subsets of $n$ of cardinality $0$ are exactly the subsets equal to $\emptyset$ (The cardinality $∣ A ∣$ of a finite set, clause (b)), so $[n]^{0} = {\emptyset}$ , a one-element set. No empty-product convention is involved.
$(\binom{n}{n}) = 1$ : if $S \subseteq n$ has $∣ S ∣ = n = ∣ n ∣$ then $S = n$ by clause 3 of A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , so $[n]^{n} = {n}$ .
$(\binom{n}{k}) = 0$ for $k > n$ : a subset $S \subseteq n$ has $∣ S ∣ \leq n$ by clause 2 of A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , so $∣ S ∣ = k > n$ is impossible and $[n]^{k} = \emptyset$ (Trichotomy of the order on $N$ ).
$(\binom{n}{1}) = n$ : a subset of cardinality $1$ is ${x}$ for exactly one $x \in n$ , since $∣ S ∣ = 1$ means $S \approx {0}$ ; so $S \mapsto$ its unique element is a bijection $[n]^{1} \to n$ .
$(\binom{0}{0}) = 1$ and $(\binom{0}{k}) = 0$ for $k \geq 1$ , both instances of the above.

Remarks

Notation. $[A]^{k}$ is standard for the set of $k$ -element subsets; it is unrelated to the notation $A^{B}$ for a set of functions, which appears on this page as well. Where confusion is possible the words are used in full.
Symmetry is not visible yet. $(\binom{n}{k}) = (\binom{n}{n - k})$ is proved in $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ by exhibiting the complementation bijection $S \mapsto n ∖ S$ ; from the definition alone there is no reason for the two counts to agree.
$0$ is a legitimate value of $k$ and of $n$ . Every boundary clause above is checked at $0$ , which is where a statement about binomial coefficients most often goes wrong in this library's index convention.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

$(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$

Statement

Let $n, k \in N$ with $k \leq n$ . Then, in $N$ ,

$(\binom{n}{k}) \cdot k! \cdot (n - k)! = n!,$

and consequently:

$(\binom{n}{k}) \cdot k! = n^{\underline{k}}$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ );
integrality: in $R$ , $ι (\binom{n}{k}) = \frac{ι (n!)}{ι (k!) ι ((n - k)!)}$ , so the familiar quotient $n! / (k! (n - k)!)$ is the canonical natural of a natural number, namely of the count $(\binom{n}{k})$ ;
symmetry: $(\binom{n}{k}) = (\binom{n}{n - k})$ .

Here $ι$ is the canonical natural of The canonical natural $ι (n) = n \cdot 1_{F}$ of a field and $n - k$ the truncated difference, which for $k \leq n$ is the ordinary one.

Facts & Assumptions

Given: Naturals $n, k$ with $k \leq n$ ; the initial segment $k = {i : i < k}$ , which satisfies $k \subseteq n$ ; and $Bij (X, Y)$ for the set of bijections $X \to Y$ .

[L1]

$(\binom{m}{j}) = ∣ [X]^{j} ∣$ for every finite $X$ with $∣ X ∣ = m$ ; $[X]^{j}$ is finite (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[L2]

$∣ Bij (X, Y) ∣ = m!$ when $∣ X ∣ = ∣ Y ∣ = m$ , and such a set is finite (A finite set $A$ with $∣ A ∣ = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality).

[L3]

[L4]

The product rule $∣ X \times Y ∣ = ∣ X ∣ ∣ Y ∣$ (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ).

[L5]

Factorials (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ): $m! \neq 0$ for every $m$ ; $n^{\underline{k}} (n - k)! = n!$ for $k \leq n$ .

[L6]

Cardinality and subsets (The cardinality $∣ A ∣$ of a finite set, A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ): transport along a bijection; $∣ m ∣ = m$ ; a subset of a finite set is finite.

[L7]

Arithmetic of $N$ : multiplication is associative and commutative, and $x \cdot c = y \cdot c$ with $c \neq 0$ gives $x = y$ (Multiplication is associative, Multiplication is commutative, Cancellation for multiplication by a nonzero factor); $k + t = n$ determines $t = n - k$ (Order on the natural numbers, Addition is cancellative).

[L8]

The embedding $ι$ is multiplicative and injective, and $ι (m) \neq 0$ for $m \neq 0$ (clauses 0 and 7 of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field); a nonzero element of a field has a unique inverse, so division by it is legitimate (Identities and inverses in a field are unique, Field).

[L9]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ): a map with a two-sided inverse is a bijection; a bijection of $n$ carries a subset onto a subset and the complement onto the complement.

Proof

technique · direct

1.1

The set to be counted twice is $Bij (n)$ , of cardinality $n!$ by [L2]. For $S \in [n]^{k}$ put ${Bij}_{S} : = {f \in Bij (n) : f [k] = S}$ . These sets are pairwise disjoint, since $f$ determines $f [k]$ , and their union over $S \in [n]^{k}$ is all of $Bij (n)$ , because $f [k]$ is a subset of $n$ of cardinality $k$ for every bijection $f$ of $n$ .

L1L2L6L9construct

1.2

For any $X \subseteq n$ with $∣ X ∣ = k$ one has $∣ n ∖ X ∣ = n - k$ : the sets $X$ and $n ∖ X$ are disjoint with union $n$ , so $n = k + ∣ n ∖ X ∣$ by [L3], and [L7] identifies the second summand as $n - k$ .

L3L6L7

2.1

$∣ {Bij}_{S} ∣ = k! (n - k)!$ for every $S \in [n]^{k}$ . Indeed $f \mapsto (f ↾ k, f ↾ (n ∖ k))$ maps ${Bij}_{S}$ to $Bij (k, S) \times Bij (n ∖ k, n ∖ S)$ : if $f [k] = S$ then $f$ restricted to $k$ is a bijection onto $S$ , and, $f$ being a bijection of $n$ , it carries $n ∖ k$ onto $n ∖ S$ . The map $(u, v) \mapsto u \cup v$ is a two-sided inverse, the union of the two functions being a function on $k \cup (n ∖ k) = n$ and a bijection onto $S \cup (n ∖ S) = n$ . Since $∣ k ∣ = ∣ S ∣ = k$ and $∣ n ∖ k ∣ = ∣ n ∖ S ∣ = n - k$ by step 1.2, [L2] and [L4] give the cardinality $k! (n - k)!$ .

step 1.1step 1.2L2L4L6L9

2.2

Symmetry. The map $S \mapsto n ∖ S$ sends $[n]^{k}$ into $[n]^{n - k}$ by step 1.2, and $T \mapsto n ∖ T$ sends $[n]^{n - k}$ into $[n]^{k}$ , again by step 1.2 together with $n - (n - k) = k$ , which holds because $(n - k) + k = n$ . The two are mutually inverse, since $n ∖ (n ∖ S) = S$ for $S \subseteq n$ . Hence $(\binom{n}{k}) = (\binom{n}{n - k})$ .

step 1.2L1L6L7L9construct

3.1

Counting $Bij (n)$ by the blocks of step 1.1 and using [L3], $n! = ∣ Bij (n) ∣ = \sum_{S \in [n]^{k}} ∣ {Bij}_{S} ∣ = \sum_{S \in [n]^{k}} k! (n - k)! = ∣ [n]^{k} ∣ \cdot k! (n - k)! = (\binom{n}{k}) k! (n - k)!$ , the summand being constant.

step 1.1step 2.1L1L3

4.1

Clause 1. By [L5], $n^{\underline{k}} (n - k)! = n!$ , so $((\binom{n}{k}) k!) (n - k)! = n^{\underline{k}} (n - k)!$ by step 3.1 and associativity; since $(n - k)! \neq 0$ , cancellation gives $(\binom{n}{k}) k! = n^{\underline{k}}$ .

step 3.1L5L7

4.2

Clause 2. Applying $ι$ to step 3.1 and using multiplicativity, $ι (n!) = ι (\binom{n}{k}) ι (k!) ι ((n - k)!)$ . Both $ι (k!)$ and $ι ((n - k)!)$ are nonzero by [L5] and [L8], so their product is invertible in $R$ and $ι (\binom{n}{k}) = ι (n!) / (ι (k!) ι ((n - k)!))$ . The left-hand side is the canonical natural of the count $(\binom{n}{k})$ , which is what the word integrality means here.

step 3.1L5L8

5.1

The displayed identity is step 3.1, clause 1 is step 4.1, clause 2 is step 4.2 and clause 3 is step 2.2.

step 2.2step 3.1step 4.1step 4.2∎

Remarks

Why the symmetry is proved by a bijection. Complementation is shorter than manipulating the closed formula, it needs no hypothesis beyond $k \leq n$ , and it is the argument that survives to the multinomial coefficient, where no single closed formula is available until the analogous count has been made.
Where $k \leq n$ is used. In step 1.1, so that $k$ is a subset of $n$ of cardinality $k$ and $[n]^{k}$ is nonempty; and in step 1.2, so that $n - k$ is a genuine difference. For $k > n$ both sides of the displayed identity are still defined, but the left-hand side is $0$ while $n!$ is not, so the hypothesis is not removable.
The quotient formula is a theorem about a natural number. A reader who starts from $n! / (k! (n - k)!)$ has to prove that the division comes out exact. Starting from the count, the exactness is what step 3.1 says, and the quotient is a consequence.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

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})$

Statement

For all $n, k \in N$ :

Pascal's rule. $(\binom{n + 1}{k + 1}) = (\binom{n}{k}) + (\binom{n}{k + 1})$ , with no restriction relating $k$ to $n$ ;
The hockey-stick identity. $\sum_{i < n + 1} (\binom{i}{k}) = (\binom{n + 1}{k + 1})$ , the sum being the $N$ -valued finite sum of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ over $i = 0, 1, \dots, n$ .

Facts & Assumptions

Given: Naturals $n$ , $k$ ; $σ (m) = m + 1$ ; and $(\binom{m}{j}) = ∣ [X]^{j} ∣$ for any finite $X$ with $∣ X ∣ = m$ .

[L1]

Induction (The principle of mathematical induction).

[L2]

Binomial coefficients (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ): $∣ [X]^{j} ∣ = (\binom{∣ X ∣}{j})$ ; $(\binom{m}{0}) = 1$ ; $(\binom{m}{j}) = 0$ for $j > m$ ; $(\binom{m}{m}) = 1$ ; $(\binom{m}{1}) = m$ .

[L3]

The sum rule for two disjoint blocks, and the recursion clause $\sum_{i < σ (n)} c_{i} = \sum_{i < n} c_{i} + c_{n}$ (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ).

[L4]

Cardinality (The cardinality $∣ A ∣$ of a finite set, A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ): transport along a bijection; a subset of a finite set is finite; $∣ {a} ∣ = 1$ ; $∣ X ∣ = 0$ exactly when $X = \emptyset$ .

[L5]

Cancellation and order in $N$ : $x + 1 = y + 1$ implies $x = y$ ; trichotomy (Addition is cancellative, Trichotomy of the order on $N$ , Order on the natural numbers).

[L6]

Maps (Injection, surjection, bijection): a map with a two-sided inverse is a bijection.

[L7]

Naturals: $σ (m) = m \cup {m}$ and $m \notin m$ (The natural numbers $N$ (von Neumann)).

Proof

technique · induction

1.1

Fix $n$ and $k$ , let $A$ be a set with $∣ A ∣ = σ (n)$ , and fix $a \in A$ , possible because $A \neq \emptyset$ by [L4]. Put $A^{'} : = A ∖ {a}$ , which is finite with $∣ A^{'} ∣ = n$ : indeed $A = A^{'} \cup {a}$ is a disjoint union, so $σ (n) = ∣ A^{'} ∣ + 1$ by [L3], and [L5] applies. Split $[A]^{σ (k)}$ into $P : = {S \in [A]^{σ (k)} : a \in S}$ and $Q : = {S \in [A]^{σ (k)} : a \notin S}$ , which are disjoint with union $[A]^{σ (k)}$ .

L3L4L5L7

1.2

The two blocks are counted by $(\binom{n}{k})$ and $(\binom{n}{σ (k)})$ . First, $Q = [A^{'}]^{σ (k)}$ , since a subset of $A$ avoiding $a$ is exactly a subset of $A^{'}$ ; so $∣ Q ∣ = (\binom{n}{σ (k)})$ by [L2]. Second, $S \mapsto S ∖ {a}$ maps $P$ into $[A^{'}]^{k}$ : for $S \in P$ the set $S$ is the disjoint union of $S ∖ {a}$ and ${a}$ , so $σ (k) = ∣ S ∖ {a} ∣ + 1$ and $∣ S ∖ {a} ∣ = k$ by [L5]. Its two-sided inverse is $T \mapsto T \cup {a}$ , which lands in $P$ because $a \notin T \subseteq A^{'}$ gives $∣ T \cup {a} ∣ = k + 1 = σ (k)$ by [L3]. Hence $∣ P ∣ = (\binom{n}{k})$ by [L2] and [L4].

L2L3L4L5L6construct

1.3

Base case of clause 2, at $n = 0$ . The left-hand side is $\sum_{i < 1} (\binom{i}{k}) = (\binom{0}{k})$ by [L3], and the right-hand side is $(\binom{1}{σ (k)})$ . If $k = 0$ both are $1$ , by $(\binom{0}{0}) = 1$ and $(\binom{1}{1}) = 1$ from [L2]. If $k \geq 1$ then $k > 0$ and $σ (k) > 1$ , so both are $0$ by [L2].

baseL2L3L5

1.4

Inductive hypothesis for clause 2: fix $n$ and assume $\sum_{i < σ (n)} (\binom{i}{k}) = (\binom{σ (n)}{σ (k)})$ for every $k$ .

2.1

Clause 1. By step 1.1, step 1.2 and the sum rule, $(\binom{σ (n)}{σ (k)}) = ∣ [A]^{σ (k)} ∣ = ∣ P ∣ + ∣ Q ∣ = (\binom{n}{k}) + (\binom{n}{σ (k)})$ . No relation between $k$ and $n$ was used, and the identity is correct beyond the range as well: for $k > n$ all three coefficients are $0$ by [L2], and at $k = 0$ it reads $(\binom{σ (n)}{1}) = 1 + (\binom{n}{1})$ , which is $σ (n) = 1 + n$ .

step 1.1step 1.2L2L3

3.1

Inductive step for clause 2. Using the recursion clause and then the hypothesis of step 1.4, $\sum_{i < σ (σ (n))} (\binom{i}{k}) = \sum_{i < σ (n)} (\binom{i}{k}) + (\binom{σ (n)}{k}) = (\binom{σ (n)}{σ (k)}) + (\binom{σ (n)}{k})$ , and clause 1 applied with $σ (n)$ in place of $n$ says exactly that this is $(\binom{σ (σ (n))}{σ (k)})$ .

step 1.4step 2.1L3

4.1

By step 1.3, step 3.1 and induction, clause 2 holds for every $n$ and every $k$ .

step 1.3step 3.1L1

5.1

Clause 1 is step 2.1 and clause 2 is step 4.1.

step 2.1step 4.1discharge-induction∎

Remarks

The rule needs no range hypothesis because the boundary values of The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ make every out-of-range coefficient $0$ rather than undefined. Both edges were checked in step 2.1 rather than assumed.
The hockey stick sums a column, not a row. The index $i$ runs over $0, 1, \dots, n$ with $k$ fixed, and the terms with $i < k$ vanish, so the identity is a statement about the entries $(\binom{k}{k}), (\binom{k + 1}{k}), \dots$ of one column of Pascal's triangle. The base case $n = 0$ is the only place where the two readings $k = 0$ and $k \geq 1$ have to be separated.
Everything here is an identity in $N$ . No embedding into $R$ is used or needed; the sum is the $N$ -valued one.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

A finite set with $n$ elements has exactly $(\binom{n}{2})$ two-element subsets, and $2 (\binom{n}{2}) = n (n - 1)$

Statement

Let $A$ be a finite set with $n : = ∣ A ∣$ . Then the set $[A]^{2}$ of two-element subsets of $A$ is finite with

$∣ [A]^{2} ∣ = (\binom{n}{2}),$

and, for every $n \in N$ , the identity

$2 \cdot (\binom{n}{2}) = n (n - 1)$

holds in $N$ , the difference being the truncated one. Equivalently, in $R$ , $ι (\binom{n}{2}) = ι (n) (ι (n) - 1) / 2$ for every $n \in N$ .

Facts & Assumptions

Given: A finite set $A$ with $n = ∣ A ∣$ , and $2 = σ (1)$ . The difference $n - 1$ is the truncated one, equal to $0$ at $n = 0$ .

[L1]

$∣ [A]^{j} ∣ = (\binom{∣ A ∣}{j})$ , $[A]^{j}$ is finite, and $(\binom{m}{j}) = 0$ for $j > m$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , The cardinality $∣ A ∣$ of a finite set).

[L2]

$(\binom{m}{j}) j! = m^{\underline{j}}$ for $j \leq m$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ , clause 1).

[L3]

Falling factorials and factorials (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ): $m^{\underline{0}} = 1$ , $m^{\underline{σ (j)}} = m^{\underline{j}} (m - j)$ , $0! = 1! = 1$ and $2! = 2$ .

[L4]

Arithmetic of $N$ : multiplication is commutative, $m \cdot 0 = 0$ , $1 \cdot m = m$ (Multiplication is commutative, Zero and one under multiplication, Multiplication of natural numbers); and $m - 0 = m$ (Order on the natural numbers).

[L5]

The embedding $ι$ is additive, multiplicative and injective, and $ι (m) > 0$ for $m \geq 1$ (clauses 0 and 7 of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field); $R$ is an ordered field, so a nonzero element is invertible (Field, Ordered field).

[L6]

Trichotomy in $N$ (Trichotomy of the order on $N$ ).

Proof

technique · direct

1.1

The first assertion is the definition: $[A]^{2}$ is finite and $∣ [A]^{2} ∣ = (\binom{n}{2})$ by [L1], because $∣ A ∣ = n$ .

1.2

The falling factorial at $2$ : $n^{\underline{1}} = n^{\underline{0}} \cdot (n - 0) = 1 \cdot n = n$ and $n^{\underline{2}} = n^{\underline{1}} \cdot (n - 1) = n (n - 1)$ , using [L3] and [L4].

L3L4

2.1

Let $n \geq 2$ . Then [L2] with $j = 2$ gives $(\binom{n}{2}) \cdot 2! = n^{\underline{2}}$ , that is $(\binom{n}{2}) \cdot 2 = n (n - 1)$ by step 1.2 and $2! = 2$ ; commutativity turns this into $2 (\binom{n}{2}) = n (n - 1)$ .

step 1.2L2L3L4

3.1

The two remaining values of $n$ . If $n = 0$ then $2 > 0$ , so $(\binom{0}{2}) = 0$ by [L1], and the right-hand side is $0 \cdot (0 - 1) = 0 \cdot 0 = 0$ by [L4]. If $n = 1$ then $2 > 1$ , so $(\binom{1}{2}) = 0$ , and the right-hand side is $1 \cdot (1 - 1) = 1 \cdot 0 = 0$ . In both cases $2 (\binom{n}{2}) = 0 = n (n - 1)$ , so with step 2.1 and trichotomy the identity holds for every $n \in N$ .

step 2.1L1L4L6

4.1

The real form. For $n \geq 1$ we have $(n - 1) + 1 = n$ , so $ι (n - 1) + 1 = ι (n)$ and $ι (n - 1) = ι (n) - 1$ ; applying $ι$ to step 3.1 then gives $ι (2) ι (\binom{n}{2}) = ι (n) (ι (n) - 1)$ , and $ι (2) = 2 \neq 0$ is invertible, so $ι (\binom{n}{2}) = ι (n) (ι (n) - 1) / 2$ . At $n = 0$ both sides are $0$ , the left by step 3.1 and the right because $ι (0) = 0$ .

step 3.1L5

5.1

The count is step 1.1, the identity in $N$ is step 3.1, and its real form is step 4.1.

step 1.1step 3.1step 4.1∎

Remarks

This is a count of unordered pairs, stated purely as a count. No geometric or relational vocabulary appears, because none is available at this point in the reading order. Later pages will want exactly this quantity, and they may cite it from here.
Both small cases are checked. At $n = 0$ and $n = 1$ there are no two-element subsets and both sides are $0$ ; the truncated difference is what makes the right-hand side come out $0$ rather than undefined at $n = 0$ .
The real form is not the definition. $ι (n) (ι (n) - 1) / 2$ is a real number that happens to be the canonical natural of a count; the identity in $N$ is the primary statement and the division is a convenience.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$

Statement

For all $x, y \in R$ and every $n \in N$ ,

$(x + y)^{n} = \sum_{k < n + 1} ι (\binom{n}{k}) x^{k} y^{n - k},$

where the powers are the integer powers of Integer powers $a^{m}$ , the sum is the real finite sum of Finite sums and finite products, by recursion over $k = 0, 1, \dots, n$ , the difference $n - k$ is a genuine one because $k \leq n$ throughout the range, and $ι$ is the canonical natural of The canonical natural $ι (n) = n \cdot 1_{F}$ of a field.

The coefficient is $ι (\binom{n}{k})$ and not $(\binom{n}{k})$ . A binomial coefficient is a natural number, that is a von Neumann natural, that is a set; it is not an element of $R$ , and it enters the field through $ι$ .

The identity is stated in $R$ and only in $R$ . The same proof uses nothing but commutativity, associativity, distributivity and natural-number multiples of a ring element, so a commutative-ring version is available wherever rings are; rings are not available at this point in the reading order, and the ring statement is a separate statement, to be made where they are. See the Remarks below.

Facts & Assumptions

Given: Reals $x, y$ ; a natural $n$ ; and the abbreviation $c_{k} : = ι (\binom{n}{k})$ for every $k \in N$ , so that $c_{k} = ι (0) = 0$ whenever $k > n$ .

[L1]

Induction (The principle of mathematical induction).

[L2]

Integer powers (Integer powers $a^{m}$ ): $a^{0} = 1$ for every real $a$ , including $a = 0$ , and $a^{σ (m)} = a^{m} \cdot a$ . An immediate induction gives $1^{m} = 1$ .

[L3]

Real finite sums (Finite sums and finite products, by recursion): $\sum_{k < 0} u_{k} = 0$ and $\sum_{k < σ (N)} u_{k} = \sum_{k < N} u_{k} + u_{N}$ ; additivity $\sum (u_{k} + v_{k}) = \sum u_{k} + \sum v_{k}$ , scaling $\sum λ u_{k} = λ \sum u_{k}$ , and splitting $\sum_{k < N} u_{k} = \sum_{k < p} u_{k} + \sum_{j < N - p} u_{p + j}$ for $p \leq N$ (Laws of finite sums and finite products, clauses 1, 2 and 3).

[L4]

$ι$ is additive and multiplicative with $ι (0) = 0$ and $ι (1) = 1$ (clause 0 of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L5]

Binomial coefficients (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ): $(\binom{m}{0}) = 1$ and $(\binom{m}{j}) = 0$ for $j > m$ ; Pascal's rule $(\binom{σ (m)}{σ (j)}) = (\binom{m}{j}) + (\binom{m}{σ (j)})$ for all $m, j$ (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})$ , clause 1).

[L6]

Field arithmetic of $R$ : associativity, commutativity, distributivity, $0 \cdot a = 0$ (Field, Ordered field, Multiplication by zero: $0 \cdot a = 0$ ).

[L7]

Arithmetic of $N$ : for $k \leq n$ , $k + (n - k) = n$ , and hence $(n - k) + 1 = σ (n) - k$ and $σ (n) - σ (k) = n - k$ ; every nonzero natural is a successor (Order on the natural numbers, Addition is cancellative, Every nonzero natural number is a successor, Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ for the truncated difference).

Proof

technique · induction

1.1

Both sides are functions of $n$ with $x, y$ fixed, and the induction is on $n$ . Note first that $c_{σ (n)} = ι (\binom{n}{σ (n)}) = ι (0) = 0$ , since $σ (n) > n$ .

givenL4L5

1.2

Base case $n = 0$ . The left-hand side is $(x + y)^{0} = 1$ by [L2]. The right-hand side is $\sum_{k < 1} ι (\binom{0}{k}) x^{k} y^{0 - k} = ι (\binom{0}{0}) x^{0} y^{0} = 1 \cdot 1 \cdot 1 = 1$ , using [L3], $(\binom{0}{0}) = 1$ , $ι (1) = 1$ and [L2]. This is correct at $x = 0$ and at $y = 0$ as well, because $a^{0} = 1$ for every real $a$ .

baseL2L3L4L5

1.3

Inductive hypothesis: fix $n$ and assume $(x + y)^{n} = \sum_{k < σ (n)} c_{k} x^{k} y^{n - k}$ for all $x, y \in R$ .

2.1

Expanding one factor. By [L2] and distributivity, $(x + y)^{σ (n)} = (x + y)^{n} (x + y) = (\sum_{k < σ (n)} c_{k} x^{k} y^{n - k}) x + (\sum_{k < σ (n)} c_{k} x^{k} y^{n - k}) y$ , using the hypothesis of step 1.3; and by the scaling clause of [L3] together with $x^{k} x = x^{σ (k)}$ and $y^{n - k} y = y^{(n - k) + 1}$ this equals $Σ_{1} + Σ_{2}$ with $Σ_{1} : = \sum_{k < σ (n)} c_{k} x^{σ (k)} y^{n - k}$ and $Σ_{2} : = \sum_{k < σ (n)} c_{k} x^{k} y^{(n - k) + 1}$ .

step 1.3L2L3L6

3.1

Rewriting $Σ_{2}$ . For $k \leq n$ one has $(n - k) + 1 = σ (n) - k$ by [L7], so $Σ_{2} = \sum_{k < σ (n)} c_{k} x^{k} y^{σ (n) - k}$ . Extending the range by one term costs nothing: by the recursion clause of [L3], $\sum_{k < σ (σ (n))} c_{k} x^{k} y^{σ (n) - k} = Σ_{2} + c_{σ (n)} x^{σ (n)} y^{0}$ , and $c_{σ (n)} = 0$ by step 1.1, so the added term is $0$ by [L6] and $Σ_{2} = \sum_{k < σ (σ (n))} c_{k} x^{k} y^{σ (n) - k}$ .

step 1.1step 2.1L3L6L7

3.2

Rewriting $Σ_{1}$ . Define a list $b$ of length $σ (σ (n))$ by $b_{0} : = 0$ and $b_{σ (i)} : = c_{i} x^{σ (i)} y^{n - i}$ for $i < σ (n)$ ; every index below $σ (σ (n))$ is $0$ or a successor $σ (i)$ with $i < σ (n)$ , by [L7], so $b$ is well defined. Splitting at $p = 1$ by [L3] and using $σ (σ (n)) - 1 = σ (n)$ and $1 + i = σ (i)$ , $\sum_{j < σ (σ (n))} b_{j} = b_{0} + \sum_{i < σ (n)} b_{σ (i)} = 0 + Σ_{1} = Σ_{1}$ .

step 2.1L3L6L7

4.1

Adding the two. By step 3.1, step 3.2 and the additivity clause of [L3], $(x + y)^{σ (n)} = \sum_{k < σ (σ (n))} (b_{k} + c_{k} x^{k} y^{σ (n) - k})$ . Evaluate the general term. At $k = 0$ it is $0 + ι (\binom{n}{0}) x^{0} y^{σ (n)} = y^{σ (n)} = ι (\binom{σ (n)}{0}) x^{0} y^{σ (n) - 0}$ , both coefficients being $ι (1) = 1$ . At $k = σ (i)$ with $i < σ (n)$ it is $c_{i} x^{σ (i)} y^{n - i} + c_{σ (i)} x^{σ (i)} y^{σ (n) - σ (i)}$ , and $σ (n) - σ (i) = n - i$ by [L7], so the term equals $(ι (\binom{n}{i}) + ι (\binom{n}{σ (i)})) x^{σ (i)} y^{σ (n) - σ (i)} = ι (\binom{σ (n)}{σ (i)}) x^{σ (i)} y^{σ (n) - σ (i)}$ by the additivity of $ι$ and Pascal's rule. Hence $(x + y)^{σ (n)} = \sum_{k < σ (σ (n))} ι (\binom{σ (n)}{k}) x^{k} y^{σ (n) - k}$ , which is the claim at $σ (n)$ .

step 3.1step 3.2L3L4L5L6L7

5.1

By step 1.2, step 4.1 and induction the identity holds for every $n \in N$ and all reals $x$ , $y$ ; in particular at $x = 0$ or $y = 0$ , where the convention $a^{0} = 1$ of Integer powers $a^{m}$ is what makes the extreme terms come out right and no exceptional case is needed.

step 1.2step 4.1L1L2discharge-induction∎

Remarks

Two index traps, both checked. The sum runs over $k < n + 1$ , that is $k \leq n$ , so the exponent $n - k$ is never a truncated difference in disguise; and the inductive step needs the coefficient $(\binom{n}{σ (n)})$ , which is $0$ by the boundary values of The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ rather than undefined. Step 1.1 records that once and both rewritings use it.
Where $0^{0}$ matters. At $x = 0$ the term with $k = 0$ is $ι (\binom{n}{0}) 0^{0} y^{n} = y^{n}$ , and the identity reads $y^{n} = y^{n}$ . A treatment leaving $0^{0}$ undefined would have to state the theorem with exceptions; Integer powers $a^{m}$ fixes $a^{0} = 1$ for every real $a$ , so there are none.
The ring version is a different statement. It says the same thing about $x, y$ in a commutative ring, with $ι (\binom{n}{k})$ replaced by the $(\binom{n}{k})$ -fold multiple of the ring element. Making it requires rings, which come later in the reading order; the pointer to Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides ↗ is orientation only and nothing above rests on it.

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

$\sum_{k < n + 1} (\binom{n}{k}) = 2^{n}$ , and $\sum_{k < n + 1} (- 1)^{k} ι ⁣ (\binom{n}{k}) = 0$ for $n \geq 1$

Statement

The row sum. For every $n \in N$ , in $N$ , $\sum_{k < n + 1} (\binom{n}{k}) = 2^{n} .$
The alternating row sum. For every $n \geq 1$ , in $R$ , $\sum_{k < n + 1} (- 1)^{k} ι (\binom{n}{k}) = 0.$

Clause 2 is false at $n = 0$ , where the sum has the single term $(- 1)^{0} ι (\binom{0}{0}) = 1$ . The hypothesis $n \geq 1$ is therefore part of the statement, and this page's companion records the version that drops it as a false statement.

Facts & Assumptions

Given: A natural $n$ , a finite set $A$ with $∣ A ∣ = n$ , and $ι$ the canonical natural (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L1]

The binomial theorem: $(x + y)^{n} = \sum_{k < σ (n)} ι (\binom{n}{k}) x^{k} y^{n - k}$ for reals $x$ , $y$ (The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ ).

[L2]

$∣ P (A) ∣ = 2^{n}$ ( $∣ P (A) ∣ = 2^{∣ A ∣}$ for finite $A$ ), and $∣ [A]^{k} ∣ = (\binom{n}{k})$ , with $[A]^{k} = \emptyset$ for $k > n$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[L3]

The sum rule for a partition indexed by a finite set (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition), the bridge $\sum_{i \in N} u_{i} = \sum_{k < N} u_{k}$ for an index set that is a natural number (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form), and the $N$ -valued recursion clauses (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ).

[L4]

$ι$ is additive, multiplicative and injective, and $ι (\sum_{k < N}^{N} a_{k}) = \sum_{k < N}^{R} ι (a_{k})$ (clauses 0, 6 and 7 of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ ).

[L5]

Powers: $ι (m^{j}) = ι (m)^{j}$ (Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ , clause (d)); $a^{0} = 1$ and $a^{σ (j)} = a^{j} a$ , so $1^{j} = 1$ and $0^{j} = 0$ for $j \geq 1$ (Integer powers $a^{m}$ , Multiplication by zero: $0 \cdot a = 0$ , Field).

[L6]

Real finite sums: the recursion clauses and the scaling clause (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L7]

Subsets of a finite set are finite and have cardinality at most $n$ (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , The cardinality $∣ A ∣$ of a finite set); induction (The principle of mathematical induction).

Proof

technique · direct

1.1

Clause 1, by counting. Every $S \subseteq A$ satisfies $∣ S ∣ \leq n$ by [L7], so $P (A)$ is the union of the sets $[A]^{k}$ for $k \in σ (n) = {0, 1, \dots, n}$ ; these are pairwise disjoint, since $S$ determines $∣ S ∣$ . By [L3] and [L2], $2^{n} = ∣ P (A) ∣ = \sum_{k \in σ (n)} ∣ [A]^{k} ∣ = \sum_{k < σ (n)} (\binom{n}{k})$ , the last equality being the bridge for an index set that is a natural number.

L2L3L7

1.2

Clause 2. Apply [L1] with $x = - 1$ and $y = 1$ . The left-hand side is $(- 1 + 1)^{n} = 0^{n}$ , which is $0$ because $n \geq 1$ ([L5]). The right-hand side is $\sum_{k < σ (n)} ι (\binom{n}{k}) (- 1)^{k} 1^{n - k} = \sum_{k < σ (n)} (- 1)^{k} ι (\binom{n}{k})$ , using $1^{j} = 1$ from [L5]. Hence the alternating sum is $0$ .

L1L5

2.1

Clause 1 again, from the binomial theorem, as a check that the two routes agree. Taking $x = y = 1$ in [L1] gives $(1 + 1)^{n} = \sum_{k < σ (n)} ι (\binom{n}{k})$ , and the right-hand side is $ι (\sum_{k < σ (n)}^{N} (\binom{n}{k}))$ by the bridge clause of [L4], while the left-hand side is $ι (2)^{n} = ι (2^{n})$ by [L5]. Since $ι$ is injective, $\sum_{k < σ (n)}^{N} (\binom{n}{k}) = 2^{n}$ , which is step 1.1.

step 1.1L1L4L5

2.2

The hypothesis of clause 2 is not removable. At $n = 0$ the sum is $\sum_{k < 1} (- 1)^{k} ι (\binom{0}{k}) = (- 1)^{0} ι (\binom{0}{0}) = 1 \cdot 1 = 1 \neq 0$ , by [L6], $(\binom{0}{0}) = 1$ and $a^{0} = 1$ . What fails in the argument of step 1.2 is exactly one thing: $(- 1 + 1)^{0} = 0^{0} = 1$ rather than $0$ .

step 1.2L2L5L6

3.1

Clause 1 is step 1.1, confirmed by step 2.1; clause 2 is step 1.2, and step 2.2 shows why it carries the hypothesis $n \geq 1$ .

step 1.1step 1.2step 2.1step 2.2∎

Remarks

Two proofs of the same identity, deliberately. The counting proof is a statement about natural numbers and uses no embedding at all, while the analytic proof goes through $R$ and comes back by the injectivity of $ι$ . Recording both is what makes the agreement of the two readings visible rather than assumed.
Where the hypothesis of clause 2 is spent. In $0^{n} = 0$ , and nowhere else. The convention $0^{0} = 1$ is not a defect here: it is what makes the binomial theorem hold at $n = 0$ , and the price is that the alternating sum identity acquires a hypothesis. Both facts are consequences of the same convention.
The alternating sum is stated in $R$ because $(- 1)^{k}$ is not a natural number. The unsigned row sum, by contrast, is an identity between counts and is stated in $N$ .

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)Open item page →

Vandermonde's identity $(\binom{m + n}{k}) = \sum_{i < k + 1} (\binom{m}{i}) (\binom{n}{k - i})$

Statement

For all $m, n, k \in N$ , in $N$ ,

$(\binom{m + n}{k}) = \sum_{i < k + 1} (\binom{m}{i}) (\binom{n}{k - i}),$

the sum running over $i = 0, 1, \dots, k$ and $k - i$ being an ordinary difference throughout that range. No restriction relating $k$ to $m$ and $n$ is needed: the terms with $i > m$ or $k - i > n$ vanish because the corresponding binomial coefficients are $0$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

Facts & Assumptions

Given: Naturals $m$ , $n$ , $k$ ; the disjoint sets $M : = m \times {0}$ and $N : = n \times {1}$ ; and $σ (k) = {0, 1, \dots, k}$ .

[L1]

Binomial coefficients (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ): $∣ [X]^{j} ∣ = (\binom{∣ X ∣}{j})$ for finite $X$ , and $[X]^{j}$ is finite.

[L2]

Cardinality (The cardinality $∣ A ∣$ of a finite set): transport along a bijection; $∣ X ∣ = ∣ Y ∣$ iff $X \approx Y$ for finite $X$ , $Y$ .

[L3]

The sum rule (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition) and the bridge $\sum_{i \in σ (k)} u_{i} = \sum_{i < σ (k)} u_{i}$ (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form, Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ).

[L4]

The product rule $∣ X \times Y ∣ = ∣ X ∣ ∣ Y ∣$ (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ).

[L5]

Subsets (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ): a subset of a finite set is finite with cardinality at most that of the set.

[L6]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ): a map with a two-sided inverse is a bijection.

[L7]

Arithmetic: if $i + t = k$ then $t = k - i$ , since $\leq$ is defined additively and addition is cancellative; and $j < σ (k) ⟺ j \leq k$ for every $j \in N$ , so $σ (k) = {0, 1, \dots, k}$ (Order on the natural numbers, Addition is cancellative, On $N$ the order is membership: $m < n ⟺ m \in n$ ). The cardinalities $∣ M ∣ = m$ and $∣ N ∣ = n$ are not assumed here; they are computed in step 1.1.

Proof

technique · direct

1.1

A disjoint pair with the right cardinalities. Put $M : = m \times {0}$ and $N : = n \times {1}$ . These are disjoint, since an element of $M$ has second coordinate $0$ and one of $N$ has second coordinate $1$ ; and $x \mapsto (x, 0)$ and $x \mapsto (x, 1)$ are bijections from $m$ and $n$ onto them, so $∣ M ∣ = m$ and $∣ N ∣ = n$ by [L2]. Hence $∣ M \cup N ∣ = m + n$ by [L3], and $∣ [M \cup N]^{k} ∣ = (\binom{m + n}{k})$ by [L1].

L1L2L3L6L7construct

1.2

The partition. For $i < σ (k)$ put $B_{i} : = {S \in [M \cup N]^{k} : ∣ S \cap M ∣ = i}$ . Every $S \in [M \cup N]^{k}$ lies in exactly one $B_{i}$ , because $S \cap M \subseteq S$ gives $∣ S \cap M ∣ \leq k$ by [L5], that is $∣ S \cap M ∣ \in σ (k)$ ; and the $B_{i}$ are pairwise disjoint since $S$ determines $∣ S \cap M ∣$ .

L1L5

2.1

Counting a block. Fix $i < σ (k)$ . The map $S \mapsto (S \cap M, S \cap N)$ sends $B_{i}$ into $[M]^{i} \times [N]^{k - i}$ : for $S \in B_{i}$ the sets $S \cap M$ and $S \cap N$ are disjoint with union $S$ , since $S \subseteq M \cup N$ , so $k = i + ∣ S \cap N ∣$ by [L3] and $∣ S \cap N ∣ = k - i$ by [L7]. The map $(U, V) \mapsto U \cup V$ is a two-sided inverse: $U \subseteq M$ and $V \subseteq N$ are disjoint, so $∣ U \cup V ∣ = i + (k - i) = k$ by [L3], and $(U \cup V) \cap M = U$ , $(U \cup V) \cap N = V$ . Hence $B_{i} \approx [M]^{i} \times [N]^{k - i}$ and $∣ B_{i} ∣ = (\binom{m}{i}) (\binom{n}{k - i})$ by [L1], [L2] and [L4].

step 1.1step 1.2L1L2L3L4L6L7construct

3.1

Adding the blocks. By step 1.2 the family $(B_{i})_{i \in σ (k)}$ is a pairwise disjoint family of finite sets with union $[M \cup N]^{k}$ , so [L3] gives $(\binom{m + n}{k}) = ∣ [M \cup N]^{k} ∣ = \sum_{i \in σ (k)} ∣ B_{i} ∣ = \sum_{i < σ (k)} (\binom{m}{i}) (\binom{n}{k - i})$ , using step 2.1 and the bridge for an index set that is a natural number.

step 1.1step 1.2step 2.1L3

4.1

No range restriction is needed: if $i > m$ then $[M]^{i} = \emptyset$ and $(\binom{m}{i}) = 0$ , and if $k - i > n$ then $(\binom{n}{k - i}) = 0$ , so those blocks are empty and contribute nothing, exactly as the identity says.

step 2.1step 3.1L1∎

Remarks

Why disjointness is arranged rather than assumed. The counting argument needs $M$ and $N$ disjoint, and two arbitrary sets of cardinalities $m$ and $n$ need not be. Replacing them by $m \times {0}$ and $n \times {1}$ costs one line and the transport clause of The cardinality $∣ A ∣$ of a finite set, and it is what makes the sum rule applicable.
Not by generating functions, and not by comparing coefficients. Both of the usual quick proofs need machinery that is far later in the reading order: formal power series in the first case, and a polynomial ring in the second. The double count needs neither.
Pascal's rule is the special case $m = 1$ , read through $(\binom{1}{0}) = (\binom{1}{1}) = 1$ and $(\binom{1}{i}) = 0$ for $i \geq 2$ : for $k \geq 1$ the identity collapses to $(\binom{1 + n}{k}) = (\binom{n}{k}) + (\binom{n}{k - 1})$ , while at $k = 0$ the sum has the single term $(\binom{1}{0}) (\binom{n}{0}) = 1 = (\binom{n + 1}{0})$ . The restriction $k \geq 1$ is not cosmetic: $n - m$ is the truncated difference throughout this page (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ), so writing the collapsed identity at $k = 0$ would read $(\binom{n}{0 - 1})$ as $(\binom{n}{0}) = 1$ and assert $1 = 1 + 1$ .

DefinitionDefinition: AI-adaptedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The multinomial coefficient $(\binom{n}{k_{0}, \dots, k_{m - 1}})$ as the number of ordered partitions of an $n$ -set into blocks of prescribed sizes

Definition

Let $m, n \in N$ . Write

$W (n, m) : = {k : m \to N ∣ \sum_{i < m} k_{i} = n},$

the set of $m$ -tuples of naturals summing to $n$ , the sum being the $N$ -valued one of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ .

$W (n, m)$ is finite. If $\sum_{i < m} k_{i} = n$ then each $k_{i} \leq n$ by the monotonicity clause of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ (a term of a sum of naturals is at most the sum), so $W (n, m)$ is a subset of the set of functions $m \to σ (n)$ , which is finite by The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ ; now apply A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ .

Block decompositions as colourings. For a finite set $A$ and $k : m \to N$ put

$B (A, k) : = {c : A \to m ∣ ∣ c^{- 1} [{i}] ∣ = k_{i} for every i < m} .$

A colouring $c$ is the same thing as an ordered decomposition of $A$ into the $m$ blocks $c^{- 1} [{0}], \dots, c^{- 1} [{m - 1}]$ ; presenting it as a function makes the blocks a partition of $A$ automatically, so that The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition and The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ apply verbatim. $B (A, k)$ is a subset of the finite set $m^{A}$ , hence finite.

The hypothesis is part of the definition, and it is forced. The fibres $c^{- 1} [{i}]$ , $i < m$ , are pairwise disjoint with union $A$ , so The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition gives $∣ A ∣ = \sum_{i < m} ∣ c^{- 1} [{i}] ∣ = \sum_{i < m} k_{i}$ for any $c \in B (A, k)$ . Hence $B (A, k) = \emptyset$ unless $k \in W (∣ A ∣, m)$ , and the coefficient is defined only under that hypothesis.

$∣ B (A, k) ∣$ depends only on $∣ A ∣$ . If $h : A \to A^{'}$ is a bijection then $c \mapsto c \circ h^{- 1}$ maps $B (A, k)$ to $B (A^{'}, k)$ , because $(c \circ h^{- 1})^{- 1} [{i}] = h [c^{- 1} [{i}]]$ has the same cardinality as $c^{- 1} [{i}]$ (The cardinality $∣ A ∣$ of a finite set); and $c^{'} \mapsto c^{'} \circ h$ is its two-sided inverse.

Definition. For $k \in W (n, m)$ set

$(\binom{n}{k_{0}, \dots, k_{m - 1}}) : = ∣ B (n, k) ∣ \in N,$

abbreviated $(\binom{n}{k})$ when the tuple is named. By the previous paragraph, $∣ B (A, k) ∣ = (\binom{∣ A ∣}{k})$ for every finite $A$ with $∣ A ∣ = n$ . Like the binomial coefficient, it is defined as a count, so it is a natural number by construction.

Boundary cases.

$m = 0$ . The empty sum is $0$ , so $W (n, 0)$ is nonempty only for $n = 0$ , where its single element is the empty tuple. And $B (\emptyset, ())$ contains exactly the empty function, so $(\binom{0}{}) = 1$ .
A block of size $0$ is allowed: $k_{i} = 0$ simply means $c^{- 1} [{i}] = \emptyset$ .
$m = 2$ recovers the binomial coefficient: for $k \leq n$ , $(\binom{n}{k, n - k}) = (\binom{n}{k})$ . The map $c \mapsto c^{- 1} [{0}]$ sends $B (A, (k, n - k))$ into $[A]^{k}$ , and $S \mapsto$ the colouring taking the value $0$ on $S$ and $1$ off it is its two-sided inverse, the second fibre having cardinality $n - k$ by The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition. So the two notations do not collide.

Remarks

Nonemptiness in the other direction. Conversely, if $k \in W (n, m)$ then $B (A, k) \neq \emptyset$ . This is not proved here and is not needed for the definition: it follows from The multinomial coefficient equals $n! / \prod_{i < m} k_{i}!$ , and $(x_{0} + \dots + x_{m - 1})^{n} = \sum ι ⁣ (\binom{n}{k}) \prod_{i < m} x_{i}^{k_{i}}$ in $R$ , whose clause 1 gives $(\binom{n}{k}) \prod_{i < m} k_{i}! = n! \neq 0$ , so the count $(\binom{n}{k})$ is nonzero and the set it counts is nonempty.
Why a colouring and not a tuple of sets. An $m$ -tuple $(S_{0}, \dots, S_{m - 1})$ of pairwise disjoint sets with union $A$ carries exactly the same information, but the disjointness and the covering would then be side conditions to be checked at every use. As fibres of a function they hold by construction.
$W (n, m)$ will get a name. Its elements are the weak compositions of $n$ into $m$ parts, and they are counted in For $m \geq 1$ the number of weak compositions of $n$ into $m$ parts is $(\binom{n + m - 1}{m - 1})$ , and the number of compositions is $(\binom{n - 1}{m - 1})$ for $n \geq 1$ ; Compositions and weak compositions of a natural number into a fixed number of parts fixes the terminology. The set is introduced here because the multinomial coefficient cannot be stated without it.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The multinomial coefficient equals $n! / \prod_{i < m} k_{i}!$ , and $(x_{0} + \dots + x_{m - 1})^{n} = \sum ι ⁣ (\binom{n}{k}) \prod_{i < m} x_{i}^{k_{i}}$ in $R$

Statement

Let $m, n \in N$ and $k \in W (n, m)$ , that is $k : m \to N$ with $\sum_{i < m} k_{i} = n$ (The multinomial coefficient $(\binom{n}{k_{0}, \dots, k_{m - 1}})$ as the number of ordered partitions of an $n$ -set into blocks of prescribed sizes). Then:

The closed formula, in $N$ . $(\binom{n}{k}) \cdot \prod_{i < m} k_{i}! = n!,$ so in $R$ the quotient $ι (n!) / \prod_{i < m} ι (k_{i}!)$ is $ι (\binom{n}{k})$ , the canonical natural of a count.
The expansion, in $R$ . For $x : m \to R$ , $(\sum_{i < m} x_{i})^{n} = \sum_{k \in W (n, m)} ι (\binom{n}{k}) \prod_{i < m} x_{i}^{k_{i}},$ the outer sum being the sum over the finite index set $W (n, m)$ (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form) and the inner product the real finite product of Finite sums and finite products, by recursion.

As with the binomial theorem, the identity is stated in $R$ ; the commutative-ring version is a separate statement, to be made where rings exist. See the Remarks of The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ .

Facts & Assumptions

Given: Naturals $m$ , $n$ , a tuple $k \in W (n, m)$ , a list $x : m \to R$ , and a finite set $A$ with $∣ A ∣ = n$ . For $m = σ (M)$ write $k^{'} : M \to N$ for the shifted tuple $k_{j}^{'} : = k_{σ (j)}$ .

[L1]

Induction (The principle of mathematical induction).

[L2]

Multinomial coefficients (The multinomial coefficient $(\binom{n}{k_{0}, \dots, k_{m - 1}})$ as the number of ordered partitions of an $n$ -set into blocks of prescribed sizes): $∣ B (A, k) ∣ = (\binom{∣ A ∣}{k})$ ; $B (A, k)$ and $W (n, m)$ are finite; $(\binom{0}{}) = 1$ for the empty tuple; and $W (n, 0)$ is ${()}$ for $n = 0$ and $\emptyset$ for $n \geq 1$ .

[L3]

The sum rule, in particular the splitting of a sum over a finite index set along a partition of that index set (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, clause 3), together with the reindexing and constant clauses of The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form.

[L4]

The binomial closed formula $(\binom{n}{j}) j! (n - j)! = n!$ for $j \leq n$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ ) and the binomial theorem (The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ ).

[L5]

Finite sums and products: the recursion clauses in $N$ and in $R$ , the splitting clause at index $1$ , and the scaling and additivity clauses in $R$ (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ , Finite sums and finite products, by recursion, Laws of finite sums and finite products, Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ ).

[L6]

Factorials: $j! \neq 0$ , and a product of nonzero naturals is nonzero; cancellation by a nonzero natural (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ , Cancellation for multiplication by a nonzero factor, Multiplication is associative, Multiplication is commutative).

[L7]

$ι$ is additive, multiplicative, injective, and commutes with finite sums and products (clauses 0, 6, 7 of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field); $R$ is a field (Field); powers obey $a^{0} = 1$ , $a^{σ (j)} = a^{j} a$ (Integer powers $a^{m}$ ).

[L8]

Binomial coefficients and cardinality: $∣ [A]^{j} ∣ = (\binom{∣ A ∣}{j})$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ); transport (The cardinality $∣ A ∣$ of a finite set); a subset of a finite set is finite (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ ); the product rule (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ); two-sided inverses give bijections (Injection, surjection, bijection); every nonzero natural is a successor (Every nonzero natural number is a successor); $j + (n - j) = n$ for $j \leq n$ (Order on the natural numbers, Addition is cancellative).

Proof

technique · induction

1.1

Notation for both inductions. For $m = σ (M)$ and $k \in W (n, σ (M))$ , splitting the sum at index $1$ ([L5]) gives $n = \sum_{i < σ (M)} k_{i} = k_{0} + \sum_{j < M} k_{j}^{'}$ , so $k^{'} \in W (n - k_{0}, M)$ and $k_{0} \leq n$ ; the same splitting for products gives $\prod_{i < σ (M)} k_{i}! = k_{0}! \cdot \prod_{j < M} k_{j}^{'}!$ .

givenL5L8

1.2

Base case of clause 1, at $m = 0$ . Then $W (n, 0)$ is nonempty only for $n = 0$ , and there $(\binom{0}{}) = 1$ , the empty product of factorials is $1$ and $0! = 1$ , so the identity reads $1 \cdot 1 = 1$ .

baseL2L5L6

1.3

Inductive hypothesis for clause 1: fix $M$ and assume $(\binom{N}{k^{'}}) \prod_{j < M} k_{j}^{'}! = N!$ for every $N$ and every $k^{'} \in W (N, M)$ .

1.4

Base case of clause 2, at $m = 0$ . The left-hand side is $(\sum_{i < 0} x_{i})^{n} = 0^{n}$ . If $n = 0$ this is $1$ , and the right-hand side is the single term $ι (\binom{0}{}) \prod_{i < 0} x_{i}^{k_{i}} = 1 \cdot 1 = 1$ . If $n \geq 1$ then $0^{n} = 0$ and $W (n, 0) = \emptyset$ , so the right-hand side is an empty sum, equal to $0$ .

L2L5L7

2.1

Inductive step for clause 1. Let $m = σ (M)$ , $k \in W (n, σ (M))$ , and let $A$ be finite with $∣ A ∣ = n$ . The map $c \mapsto (c^{- 1} [{0}], c^{''})$ , where $c^{''} (a)$ is the unique $i$ with $c (a) = σ (i)$ for $a \notin c^{- 1} [{0}]$ , sends $B (A, k)$ to the set of pairs $(S, c^{''})$ with $S \in [A]^{k_{0}}$ and $c^{''} \in B (A ∖ S, k^{'})$ ; it is well defined because $c (a) \neq 0$ off the first fibre, every nonzero natural is a unique successor, and $∣ c^{'' - 1} [{j}] ∣ = ∣ c^{- 1} [{σ (j)}] ∣ = k_{j}^{'}$ . Its two-sided inverse sends $(S, c^{''})$ to the colouring equal to $0$ on $S$ and to $σ (c^{''} (a))$ off $S$ . The pairs form the union of the pairwise disjoint sets ${S} \times B (A ∖ S, k^{'})$ indexed by $S \in [A]^{k_{0}}$ , and $∣ A ∖ S ∣ = n - k_{0}$ by [L3], so each has $(\binom{n - k_{0}}{k^{'}})$ elements. Hence $(\binom{n}{k}) = (\binom{n}{k_{0}}) (\binom{n - k_{0}}{k^{'}})$ by [L3] and [L8]. Multiplying by $\prod_{i < σ (M)} k_{i}! = k_{0}! \prod_{j < M} k_{j}^{'}!$ and using the hypothesis of step 1.3 at $N = n - k_{0}$ gives $(\binom{n}{k}) \prod_{i < σ (M)} k_{i}! = (\binom{n}{k_{0}}) k_{0}! \cdot ((\binom{n - k_{0}}{k^{'}}) \prod_{j < M} k_{j}^{'}!) = (\binom{n}{k_{0}}) k_{0}! (n - k_{0})! = n!$ by [L4], since $k_{0} \leq n$ .

step 1.1step 1.3L2L3L4L6L8construct

3.1

Clause 1 holds for every $m$ , by step 1.2, step 2.1 and induction. The real form follows: applying $ι$ gives $ι (\binom{n}{k}) \prod_{i < m} ι (k_{i}!) = ι (n!)$ , and each $ι (k_{i}!)$ is nonzero by [L6] and [L7], so the product is invertible in $R$ .

step 1.2step 2.1L1L6L7

4.1

Inductive step for clause 2. Assume clause 2 at $M$ , for every $n$ and every list of length $M$ . Let $x : σ (M) \to R$ , put $y : = \sum_{i < M} x_{i}$ and $z : = x_{M}$ , so $\sum_{i < σ (M)} x_{i} = y + z$ by [L5]. The map $Φ (j, κ) : = \hat{κ}$ , where $\hat{κ}$ restricts to $κ$ on $M$ and ${\hat{κ}}_{M} : = n - j$ , is a bijection from the disjoint union of the sets ${j} \times W (j, M)$ , $j < σ (n)$ , onto $W (n, σ (M))$ : it lands there because $\sum_{i < σ (M)} {\hat{κ}}_{i} = j + (n - j) = n$ , and its inverse sends $\hat{κ}$ to the pair $(\sum_{i < M} {\hat{κ}}_{i}, \hat{κ} ↾ M)$ , the two constructions being mutually inverse by [L8]. Moreover $ι (\binom{n}{j}) ι (\binom{j}{κ}) = ι (\binom{n}{\hat{κ}})$ : by step 3.1 and [L4], both $(\binom{n}{\hat{κ}})$ and $(\binom{n}{j}) (\binom{j}{κ})$ become $n!$ after multiplication by the nonzero natural $(\prod_{i < M} κ_{i}!) (n - j)!$ , so they are equal by cancellation. And $\prod_{i < M} x_{i}^{κ_{i}} \cdot z^{n - j} = \prod_{i < σ (M)} x_{i}^{{\hat{κ}}_{i}}$ by the product recursion clause. Now [L4] gives $(y + z)^{n} = \sum_{j < σ (n)} ι (\binom{n}{j}) y^{j} z^{n - j}$ ; substituting the inductive hypothesis for $y^{j}$ , distributing the scalar $ι (\binom{n}{j}) z^{n - j}$ over the inner sum by the scaling clause of [L5], and then applying [L3] to the partition of $W (n, σ (M))$ into the images of the sets $W (j, M)$ under $Φ$ yields $(\sum_{i < σ (M)} x_{i})^{n} = \sum_{\hat{κ} \in W (n, σ (M))} ι (\binom{n}{\hat{κ}}) \prod_{i < σ (M)} x_{i}^{{\hat{κ}}_{i}}$ .

step 1.4step 3.1assume-hypL2L3L4L5L6L7L8construct

5.1

By step 1.4, step 4.1 and induction, clause 2 holds for every $m \in N$ , every $n$ and every list $x$ .

step 1.4step 4.1L1

6.1

Clause 1 is step 3.1 and clause 2 is step 5.1.

step 3.1step 5.1discharge-induction∎

Remarks

The index set of the outer sum has to be finite, and it is. It is $W (n, m)$ , which The multinomial coefficient $(\binom{n}{k_{0}, \dots, k_{m - 1}})$ as the number of ordered partitions of an $n$ -set into blocks of prescribed sizes shows finite by injecting it into the set of functions $m \to σ (n)$ . Without that the outer sum would not be defined, which is the reason The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form exists.
The small cases are computed, not waved at. At $m = 0$ the left-hand side is $0^{n}$ and the right-hand side is an empty sum or a single term, and the two match only because $0^{0} = 1$ . At $m = 1$ the only tuple is $k = (n)$ , the coefficient is $(\binom{n}{n}) = 1$ by clause 1, and the identity reads $x_{0}^{n} = x_{0}^{n}$ .
Clause 1 is again an identity between natural numbers, so integrality of $n! / \prod k_{i}!$ is free; the quotient form is a consequence obtained through $ι$ , exactly as for the binomial coefficient.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

Compositions and weak compositions of a natural number into a fixed number of parts

Definition

Let $n, m \in N$ .

A weak composition of $n$ into $m$ parts is a function $k : m \to N$ with $\sum_{i < m} k_{i} = n$ , the sum being the $N$ -valued one of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ . The set of them is the set $W (n, m)$ introduced in The multinomial coefficient $(\binom{n}{k_{0}, \dots, k_{m - 1}})$ as the number of ordered partitions of an $n$ -set into blocks of prescribed sizes.
A composition of $n$ into $m$ parts is a weak composition all of whose parts are nonzero, that is $k_{i} \geq 1$ for every $i < m$ (Discreteness: $σ (n)$ is the immediate successor). Write $C (n, m) : = {k \in W (n, m) : k_{i} \geq 1 for every i < m} .$

The parts are ordered: $k$ is a function on $m$ , so $(1, 2)$ and $(2, 1)$ are different compositions of $3$ into $2$ parts.

Both sets are finite. Every $k \in W (n, m)$ has $k_{i} \leq n$ for each $i$ , because a term of a sum of naturals is at most the sum (clause 4 of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ ); so $W (n, m)$ is a subset of the set of functions $m \to σ (n)$ , which is finite by The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ , and A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ applies. $C (n, m)$ is a subset of $W (n, m)$ , hence finite too.

The case $m = 0$ , which is exactly where the next item's hypothesis lives. There is precisely one function $0 \to N$ , the empty function, and its sum is the empty sum, $0$ . Hence

$∣ W (0, 0) ∣ = 1, ∣ W (n, 0) ∣ = 0 for n \geq 1,$

and the same two values for $C$ , since the condition "every part is nonzero" is vacuous for the empty tuple. Saying this here is what lets For $m \geq 1$ the number of weak compositions of $n$ into $m$ parts is $(\binom{n + m - 1}{m - 1})$ , and the number of compositions is $(\binom{n - 1}{m - 1})$ for $n \geq 1$ carry the hypothesis $m \geq 1$ honestly: at $m = 0$ the count is not given by the formula, and the true value is recorded above.

Small values of $m$ . $∣ W (n, 1) ∣ = 1$ , the unique weak composition being $k_{0} = n$ ; and $∣ C (n, 1) ∣ = 1$ for $n \geq 1$ while $C (0, 1) = \emptyset$ .

Remarks

The same object under two names. $W (n, m)$ is the index set of the outer sum of The multinomial coefficient equals $n! / \prod_{i < m} k_{i}!$ , and $(x_{0} + \dots + x_{m - 1})^{n} = \sum ι ⁣ (\binom{n}{k}) \prod_{i < m} x_{i}^{k_{i}}$ in $R$ . That theorem and this definition therefore speak about one set, and the count supplied by For $m \geq 1$ the number of weak compositions of $n$ into $m$ parts is $(\binom{n + m - 1}{m - 1})$ , and the number of compositions is $(\binom{n - 1}{m - 1})$ for $n \geq 1$ is the number of terms in the multinomial expansion.
Weak versus strict. Much of the literature reserves composition for tuples of positive parts and says weak composition when zeros are allowed; that is the convention adopted here. The count of the weak ones is the primary result, and the strict count is obtained from it by subtracting $1$ from every part.
Nothing here is about unordered partitions. The number of ways of writing $n$ as an unordered sum is a different and much harder count, and it is not developed at this point in the reading order.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

For $m \geq 1$ the number of weak compositions of $n$ into $m$ parts is $(\binom{n + m - 1}{m - 1})$ , and the number of compositions is $(\binom{n - 1}{m - 1})$ for $n \geq 1$

Statement

Let $m \geq 1$ and write $m = σ (M)$ , so $M = m - 1$ . Then for every $n \in N$

$∣ W (n, m) ∣ = (\binom{n + m - 1}{m - 1}) = (\binom{n + M}{M}),$

and the map $k \mapsto {(\sum_{j < σ (i)} k_{j}) + i : i < M}$ is a bijection of $W (n, m)$ onto the set of $M$ -element subsets of $n + M$ .

Moreover, for $m \geq 1$ and $n \geq 1$ ,

$∣ C (n, m) ∣ = (\binom{n - 1}{m - 1}) .$

The hypothesis $m \geq 1$ is not decoration. At $m = 0$ the expression $(\binom{n + m - 1}{m - 1})$ would require the value $m - 1$ at $m = 0$ , and Compositions and weak compositions of a natural number into a fixed number of parts records the true counts there: $∣ W (0, 0) ∣ = 1$ and $∣ W (n, 0) ∣ = 0$ for $n \geq 1$ . The hypothesis $n \geq 1$ in the second display is equally load bearing: at $n = 0$ , $m = 1$ the formula would give $(\binom{0}{0}) = 1$ while $C (0, 1) = \emptyset$ .

Facts & Assumptions

Given: Naturals $n$ and $m = σ (M)$ with $M \in N$ ; the sets $W (n, m)$ and $C (n, m)$ of Compositions and weak compositions of a natural number into a fixed number of parts; and the truncated difference of Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ .

[L1]

Induction (The principle of mathematical induction).

[L2]

Finite sums in $N$ (Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ , Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ ): the recursion clauses; additivity; the constant clause $\sum_{k < N} c = N \cdot c$ ; splitting at $p \leq N$ ; and the fact that a partial sum $\sum_{j < P} k_{j}$ with $P \leq N$ satisfies $\sum_{j < P} k_{j} \leq \sum_{j < N} k_{j}$ , which is splitting together with $x \leq x + t$ .

[L3]

Binomial coefficients (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ): $∣ [X]^{j} ∣ = (\binom{∣ X ∣}{j})$ ; $(\binom{N}{0}) = 1$ ; $(\binom{N}{j}) = 0$ for $j > N$ .

[L4]

The hockey-stick identity $\sum_{i < σ (N)} (\binom{i}{j}) = (\binom{σ (N)}{σ (j)})$ (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})$ , clause 2).

[L5]

The sum rule and sums over a finite index set (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form).

[L6]

Cardinality and subsets (The cardinality $∣ A ∣$ of a finite set, A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ): transport; a subset of a finite set is finite; a subset of the same cardinality as the whole is the whole.

[L7]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ): a map with a two-sided inverse is a bijection; an injection is a bijection onto its image.

[L8]

Arithmetic and order in $N$ : $σ (a) = a + 1$ ; $a + σ (b) = σ (a + b)$ ; addition is commutative and cancellative; $a \leq b$ and $b \leq c$ give $a \leq c$ ; trichotomy; $a \neq 0$ is the same as $1 \leq a$ (Order on the natural numbers, Addition is cancellative, Addition is commutative, Order is compatible with addition, Trichotomy of the order on $N$ , Discreteness: $σ (n)$ is the immediate successor, The natural numbers $N$ (von Neumann)).

[L9]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

Proof

technique · induction

1.1

The last-part decomposition, valid for every $M \in N$ and every $n$ . The map $k \mapsto (\sum_{i < M} k_{i}, k ↾ M)$ sends $W (n, σ (M))$ into the union of the pairwise disjoint sets ${j} \times W (j, M)$ for $j < σ (n)$ : writing $j : = \sum_{i < M} k_{i}$ , the recursion clause gives $j + k_{M} = n$ , so $j \leq n$ and $k ↾ M \in W (j, M)$ . Its two-sided inverse sends $(j, κ)$ to the tuple extending $κ$ by the value $n - j$ at $M$ , whose sum is $j + (n - j) = n$ . Hence $∣ W (n, σ (M)) ∣ = \sum_{j < σ (n)} ∣ W (j, M) ∣$ by [L5].

L2L5L7L8construct

1.2

Base case, $M = 0$ , that is $m = 1$ . A weak composition of $n$ into one part is a function $k : 1 \to N$ with $\sum_{i < 1} k_{i} = k_{0} = n$ , and there is exactly one such function; so $∣ W (n, 1) ∣ = 1 = (\binom{n + 0}{0})$ by [L3].

baseL2L3

1.3

Inductive hypothesis: fix $M$ and assume $∣ W (n, σ (M)) ∣ = (\binom{n + M}{M})$ for every $n \in N$ .

1.4

A reindexing identity: $\sum_{j < σ (n)} (\binom{j + M}{M}) = \sum_{i < σ (n + M)} (\binom{i}{M})$ . Split the right-hand side at $p = M$ , legitimate since $M \leq σ (n + M)$ : it becomes $\sum_{i < M} (\binom{i}{M}) + \sum_{j < σ (n + M) - M} (\binom{M + j}{M})$ . The first sum vanishes, every term being $(\binom{i}{M}) = 0$ for $i < M$ by [L3] and a sum of zeros being $0$ by the constant clause; and $σ (n + M) - M = σ (n)$ , because $M + σ (n) = σ (M + n) = σ (n + M)$ .

L2L3L8

2.1

Inductive step. Applying step 1.1 with $σ (M)$ in place of $M$ , then the hypothesis of step 1.3, then step 1.4 and finally the hockey-stick identity [L4] with $N = n + M$ and $j = M$ : $∣ W (n, σ (σ (M))) ∣ = \sum_{j < σ (n)} ∣ W (j, σ (M)) ∣ = \sum_{j < σ (n)} (\binom{j + M}{M}) = \sum_{i < σ (n + M)} (\binom{i}{M}) = (\binom{σ (n + M)}{σ (M)}) = (\binom{n + σ (M)}{σ (M)})$ , the last equality because $σ (n + M) = n + σ (M)$ . That is the claim at $σ (M)$ .

step 1.1step 1.3step 1.4L4L8

3.1

By step 1.2, step 2.1 and induction, $∣ W (n, σ (M)) ∣ = (\binom{n + M}{M})$ for every $M$ and every $n$ , which is the first display since $m = σ (M)$ and $M = m - 1$ .

step 1.2step 2.1L1

4.1

The explicit bijection. For $k \in W (n, σ (M))$ and $i < M$ put $s_{i} : = (\sum_{j < σ (i)} k_{j}) + i$ and $S (k) : = {s_{i} : i < M}$ . The list is strictly increasing, since $s_{σ (i)} = (\sum_{j < σ (i)} k_{j} + k_{σ (i)}) + σ (i) = s_{i} + k_{σ (i)} + 1$ ; and $s_{i} < n + M$ , since $\sum_{j < σ (i)} k_{j} \leq \sum_{j < σ (M)} k_{j} = n$ by [L2] and $i \leq M - 1$ . So $S (k)$ is a subset of $n + M$ with exactly $M$ elements, and $S$ maps $W (n, σ (M))$ into $[n + M]^{M}$ . It is injective: a strictly increasing list enumerating a finite subset of $N$ is determined by that subset, since its first entry is the least element and each later entry is the least element strictly above the previous one ([L9] and induction), so $S (k) = S (\tilde{k})$ forces $s_{i} = {\tilde{s}}_{i}$ for all $i < M$ ; then $k_{0} = s_{0}$ and $k_{σ (i)} = s_{σ (i)} - s_{i} - 1$ recover $k$ on $M$ , and $k_{M} = n - \sum_{j < M} k_{j}$ recovers the last part. Since both sets have $(\binom{n + M}{M})$ elements by step 3.1 and [L3], the image of $S$ is a subset of $[n + M]^{M}$ of the same cardinality, hence all of it by [L6]. So $S$ is a bijection.

step 3.1L2L3L6L7L8L9construct

4.2

The count of compositions, for $m = σ (M) \geq 1$ and $n \geq 1$ . If $m \leq n$ , the map $k \mapsto k^{'}$ with $k_{i}^{'} : = k_{i} - 1$ sends $C (n, m)$ into $W (n - m, m)$ : each $k_{i} \geq 1$ , so $k_{i} = k_{i}^{'} + 1$ , and $\sum_{i < m} k_{i} = \sum_{i < m} k_{i}^{'} + \sum_{i < m} 1 = \sum_{i < m} k_{i}^{'} + m$ by additivity and the constant clause, whence $\sum_{i < m} k_{i}^{'} = n - m$ . Its two-sided inverse adds $1$ to every part. So $∣ C (n, m) ∣ = ∣ W (n - m, m) ∣ = (\binom{(n - m) + M}{M})$ by step 3.1, and $(n - m) + M = n - 1$ because $(n - m) + m = n$ and $M = m - 1$ with $m \geq 1$ . If instead $m > n$ , then every $k \in C (n, m)$ would satisfy $n = \sum_{i < m} k_{i} \geq \sum_{i < m} 1 = m$ by monotonicity, which is false; so $C (n, m) = \emptyset$ , and $(\binom{n - 1}{m - 1}) = 0$ as well, since $m > n \geq 1$ gives $m - 1 > n - 1$ . In both cases $∣ C (n, m) ∣ = (\binom{n - 1}{m - 1})$ .

step 3.1L2L3L6L7L8

5.1

The count of weak compositions is step 3.1, the bijection realising it is step 4.1, and the count of compositions is step 4.2.

step 3.1step 4.1step 4.2discharge-induction∎

Remarks

The picture behind $S$ . Lay out $n$ stars and $M$ bars in a row of $n + M$ places; the bars split the stars into $σ (M) = m$ runs, whose lengths are the parts. The set $S (k)$ is the set of positions of the bars, and step 4.1 is that picture made precise. Surjectivity is obtained from the count rather than by constructing the inverse directly, which spares an appeal to the increasing enumeration of an arbitrary subset.

tikz \begin{tikzpicture}[x=0.85cm,y=1cm] \node at (2.55,1.25) {$k=(2,0,3)$}; \node at (0,0) {$\star$}; \node at (0.85,0) {$\star$}; \draw[line width=1pt] (1.7,-0.3) -- (1.7,0.3); \draw[line width=1pt] (2.55,-0.3) -- (2.55,0.3); \node at (3.4,0) {$\star$}; \node at (4.25,0) {$\star$}; \node at (5.1,0) {$\star$}; \node at (0,-0.65) {$0$}; \node at (0.85,-0.65) {$1$}; \node at (1.7,-0.65) {$2$}; \node at (2.55,-0.65) {$3$}; \node at (3.4,-0.65) {$4$}; \node at (4.25,-0.65) {$5$}; \node at (5.1,-0.65) {$6$}; \node at (2.55,-1.35) {$S(k)=\{2,3\}\subseteq 7$}; \end{tikzpicture}

Why the count is proved by induction and not by the bijection alone. Building the inverse of $S$ by hand needs the increasing enumeration of an arbitrary $M$ -element subset of $n + M$ , which is more machinery than the hockey-stick induction. The induction gives the number, and the number then gives the surjectivity of $S$ .
Both hypotheses are visible. The failure at $m = 0$ is recorded on the companion page as a false statement; the failure at $n = 0$ of the composition formula is recorded in the Statement above.

RemarkRemark: AI-generatedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

Conventions fixed on this page, and what counting is deliberately not done here

This item is the page's ledger: every convention the page fixes, with the item that fixes it, and a statement of what is deliberately left to later pages.

Conventions fixed here

$N$ contains $0$ . Every index range on this page starts at $0$ , so $\sum_{k < n}$ runs over $k = 0, \dots, n - 1$ and $\sum_{k < n + 1}$ over $k = 0, \dots, n$ . A cardinality may be $0$ , a part of a composition may be $0$ , and a claim true only from the second index onwards is false as stated. Three items exist only because of this: the alternating row sum of $\sum_{k < n + 1} (\binom{n}{k}) = 2^{n}$ , and $\sum_{k < n + 1} (- 1)^{k} ι ⁣ (\binom{n}{k}) = 0$ for $n \geq 1$ carries the hypothesis $n \geq 1$ , For $m \geq 1$ the number of weak compositions of $n$ into $m$ parts is $(\binom{n + m - 1}{m - 1})$ , and the number of compositions is $(\binom{n - 1}{m - 1})$ for $n \geq 1$ carries $m \geq 1$ , and the composition count carries $n \geq 1$ .

$∣ A ∣$ is defined for finite $A$ only, and is a natural number. The cardinality $∣ A ∣$ of a finite set fixes this, and what makes it well posed is claim 3 of the pigeonhole principle. It is not a cardinal number: Cardinal (initial ordinal) and cardinality ↗ is a later and different object and nothing here uses it or any cardinal arithmetic.

The empty sum is $0$ , the empty product is $1$ , $0! = 1$ and $0^{0} = 1$ are one convention. Each is the base clause of a recursion carried out on this page, in Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ , The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ and Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ respectively, and each agrees with the already-published Finite sums and finite products, by recursion and Integer powers $a^{m}$ . Nothing was imported and nothing was stipulated twice.

Counts live in $N$ ; identities involving subtraction or division live in $R$ . A natural number is a von Neumann natural, hence a set, and is not an element of $R$ ; it enters through the canonical natural $ι$ . That is why the binomial theorem's coefficient is $ι (\binom{n}{k})$ , and why Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ proves that $ι$ commutes with finite sums and products and is injective. Injectivity is the licence to prove an identity between counts by proving it in $R$ .

$(\binom{n}{k})$ is a count, and integrality is a theorem. The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ defines it as $∣ [n]^{k} ∣$ , so it is a natural number by construction; that it also equals $n! / (k! (n - k)!)$ is $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ . The same holds for the multinomial coefficient (The multinomial coefficient $(\binom{n}{k_{0}, \dots, k_{m - 1}})$ as the number of ordered partitions of an $n$ -set into blocks of prescribed sizes).

Three notions of finite sum will coexist in the library, and each is introduced with a bridge to the previous one: over an initial segment (Finite sums and finite products, by recursion), over a finite index set (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form, well posed because of A finite sum is unchanged by a permutation of its index range: $\sum_{k < n} a_{π (k)} = \sum_{k < n} a_{k}$ for every bijection $π : n \to n$ ), and in an arbitrary monoid (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity ↗, later in the reading order). The bridges are what stop them drifting into three unrelated notions.

Truncated difference. On this page $n - m$ always means the unique $j$ with $m + j = n$ when $m \leq n$ , and $0$ otherwise. No negative number is ever formed, and each statement true only under $m \leq n$ says so.

What is deliberately not here

These are statements about the reading order, not about the library as a whole.

Inclusion and exclusion, the systematic repair of a count whose blocks overlap. The sum rule needs disjointness, and the companion page shows what goes wrong without it; the correction term belongs to the next page of this track.
The number of surjections, and the counting of set partitions and of unordered partitions of an integer. All are natural sequels to the material here and none is available yet.
The binomial theorem for a commutative ring. The proof given here uses only commutativity, associativity, distributivity and natural-number multiples, so the ring statement is true; it cannot be stated until rings exist (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides ↗).
Group vocabulary for $Bij (A)$ . The count $n!$ is proved here, about a set of bijections. The group structure and the name symmetric group are The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition ↗, later in the reading order, and a page there may cite the count from here.
Asymptotics of $n!$ , Stirling's formula among them. These need the logarithm and a good deal of integration, all far later in the reading order.

Every forward pointer above is orientation only: no item on this page depends on anything named in this section.

5 · Examples, counterexamples and false statements

None yet.

Finite Counting, Factorials and Binomial Coefficients

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

The cardinality ∣A∣∣A∣ of a finite set

Definition

Remarks

A subset of a finite set is finite, with ∣B∣≤∣A∣∣B∣≤∣A∣, and equality holds if and only if B=AB=A

Statement

Facts & Assumptions

Proof

Remarks

Finite sums and finite products of natural numbers, ∑k<nak∑k<n​ak​ and ∏k<nak∏k<n​ak​ in NN

Definition

Remarks

Laws of finite sums and products in NN, and ι(∑k<nak)=∑k<nι(ak)ι(∑k<n​ak​)=∑k<n​ι(ak​)

Statement

Facts & Assumptions

Proof

Remarks

A finite sum is unchanged by a permutation of its index range: ∑k<naπ(k)=∑k<nak∑k<n​aπ(k)​=∑k<n​ak​ for every bijection π:n→nπ:n→n

Statement

Facts & Assumptions

Proof

Remarks

The sum ∑i∈Sai∑i∈S​ai​ over a finite index set, and its product form

Definition

Remarks

The sum rule: a finite disjoint union is finite with ∣A∪B∣=∣A∣+∣B∣∣A∪B∣=∣A∣+∣B∣ and ∣⋃i∈IAi∣=∑i∈I∣Ai∣∣⋃i∈I​Ai​∣=∑i∈I​∣Ai​∣, and a sum over a finite index set splits along a partition

Statement

Facts & Assumptions

Proof

Remarks

The product rule: ∣A×B∣=∣A∣ ∣B∣∣A×B∣=∣A∣∣B∣, and ∣∏i<mAi∣=∏i<m∣Ai∣​∏i<m​Ai​​=∏i<m​∣Ai​∣

Statement

Facts & Assumptions

Proof

Remarks

Exponentiation of natural numbers, mnmn, and its agreement with the integer power in RR

Definition

Remarks

The set ABAB of functions B→AB→A between finite sets is finite, with ∣AB∣=∣A∣∣B∣∣AB∣=∣A∣∣B∣

Statement

Facts & Assumptions

Proof

Remarks

∣P(A)∣=2∣A∣∣P(A)∣=2∣A∣ for finite AA

Statement

Facts & Assumptions

Proof

Remarks

The factorial n!n! and the falling factorial nk‾nk​, defined by recursion in NN

Definition

Remarks

The number of injections from a kk-element set into an nn-element set is nk‾nk​

Statement

Facts & Assumptions

Proof

Remarks

A finite set AA with ∣A∣=n∣A∣=n has exactly n!n! bijections onto itself, and n!n! bijections onto any set of the same cardinality

Statement

Facts & Assumptions

Proof

Remarks

The set [A]k[A]k of kk-element subsets and the binomial coefficient (nk):=∣[n]k∣(kn​):=∣[n]k∣

Definition

Remarks

(nk) k! (n−k)!=n!(kn​)k!(n−k)!=n! for k≤nk≤n; hence (nk) k!=nk‾(kn​)k!=nk​, the quotient n!/(k!(n−k)!)n!/(k!(n−k)!) is a natural number, and (nk)=(nn−k)(kn​)=(n−kn​)

Statement

Facts & Assumptions

Proof

Remarks

Pascal's rule (n+1k+1)=(nk)+(nk+1)(k+1n+1​)=(kn​)+(k+1n​), and the hockey-stick identity ∑i≤n(ik)=(n+1k+1)∑i≤n​(ki​)=(k+1n+1​)

Statement

Facts & Assumptions

Proof

Remarks

A finite set with nn elements has exactly (n2)(2n​) two-element subsets, and 2(n2)=n(n−1)2(2n​)=n(n−1)

Statement

The cardinality $∣ A ∣$ of a finite set

A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$

Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$

Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$

A finite sum is unchanged by a permutation of its index range: $\sum_{k < n} a_{π (k)} = \sum_{k < n} a_{k}$ for every bijection $π : n \to n$

The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form

The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition

The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$

Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$

The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$

$∣ P (A) ∣ = 2^{∣ A ∣}$ for finite $A$

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$

The number of injections from a $k$ -element set into an $n$ -element set is $n^{\underline{k}}$

A finite set $A$ with $∣ A ∣ = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality

The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$

$(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$

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})$

A finite set with $n$ elements has exactly $(\binom{n}{2})$ two-element subsets, and $2 (\binom{n}{2}) = n (n - 1)$

The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$

$\sum_{k < n + 1} (\binom{n}{k}) = 2^{n}$ , and $\sum_{k < n + 1} (- 1)^{k} ι ⁣ (\binom{n}{k}) = 0$ for $n \geq 1$

Vandermonde's identity $(\binom{m + n}{k}) = \sum_{i < k + 1} (\binom{m}{i}) (\binom{n}{k - i})$

The multinomial coefficient $(\binom{n}{k_{0}, \dots, k_{m - 1}})$ as the number of ordered partitions of an $n$ -set into blocks of prescribed sizes

The multinomial coefficient equals $n! / \prod_{i < m} k_{i}!$ , and $(x_{0} + \dots + x_{m - 1})^{n} = \sum ι ⁣ (\binom{n}{k}) \prod_{i < m} x_{i}^{k_{i}}$ in $R$

For $m \geq 1$ the number of weak compositions of $n$ into $m$ parts is $(\binom{n + m - 1}{m - 1})$ , and the number of compositions is $(\binom{n - 1}{m - 1})$ for $n \geq 1$