Combinatorics · existing Mathlib declaration

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

The theorem at a glance

Euler’s Odd–Distinct Partition Theorem at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

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.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

Selected after original-pixel inspection of the theorem schematic scientific; theorem-specific structure, legibility, margins, and public claim boundary passed. — For each natural n, the odd-part and distinct-part families have the same number of partitions.

Complementary intuition

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.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

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

Selected evidence declaration text

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

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

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

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.

Provenance

Origin and evidence stay separate

Existing declaration: Nat.Partition.card_odds_eq_card_distincts in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.euler-odd-distinct-partitions.v001
Source handling: Verified upstream reference; no mirrored source package