Existing in Mathlib · Combinatorics

Euler’s Odd–Distinct Partition Theorem

Fix a natural number n. Count the partitions of n made only from odd numbers, allowing repeats. Then count the partitions of n in which no number repeats, allowing both odd and even parts. Euler’s theorem says the two counts are always equal.

integer partitions
odd parts
distinct parts
generating functions
Glaisher’s theorem

Exact theorem

Exact Mathlib statement

theorem Nat.Partition.card_odds_eq_card_distincts (n : ℕ) : #(Nat.Partition.odds n) = #(Nat.Partition.distincts n)

The theorem at a glance

Euler’s Odd–Distinct Partition Theorem at a glance

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

A portrait editorial theorem poster states the equality between counts of odd-part and distinct-part partitions and follows the checked generating-function route through Glaisher’s theorem at m equals two. — The generating functions agree, so every coefficient counts equally many odd-part and distinct-part partitions.

Statement structure

Statement and scope

Read the exact Mathlib declaration

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

Odd-part multiplicity factors and distinct-part choice factors feed equal generating products; matching coefficients of Xⁿ give equal numbers of the two partition types. — For each natural n, the odd-part and distinct-part families have the same number of partitions.

Why it matters

A mathematical landmark

Euler’s odd-versus-distinct partition identity is a foundational equinumerosity theorem in enumerative combinatorics. The Mathlib endpoint is concise, but it rests on a substantial generating-function development proving Glaisher’s more general restriction theorem and then specializing it at two.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

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

Claim boundary

No new theorem is claimed

This page indexes Mathlib’s cardinality form of Euler’s partition theorem. For every natural n, odds n is the finite set of partitions of n all of whose parts are odd, while distincts n is the finite set of partitions of n whose parts multiset has no repetitions. The declaration says that these two finite sets have equal cardinality. It does not itself construct an explicit bijection, enumerate either family, or state a broader partition identity.

The selected declaration proves equality of cardinalities, not an explicit bijection between individual partitions.
The odd-parts family allows repetitions; only the numerical value of every part must be odd.
The distinct-parts family permits even parts; its restriction is that no part repeats.
The checked source proves the result through generating functions and Glaisher’s theorem specialized to m = 2.
ProofAtlas is indexing an existing Mathlib theorem, not claiming new mathematics.

Source and local evidence

Where the theorem comes from

Existing declaration: Nat.Partition.card_odds_eq_card_distincts in mathlib
Relationship: The checked artifact is the upstream declaration itself
Local Lean evidence: artifact.library.mathlib.euler-odd-distinct-partitions.v001
Source: Open the pinned upstream reference