Existing in Mathlib · Number theory

Möbius Inversion

Suppose g records the sum of f over every positive divisor of n. Then f can be recovered by summing the values of g along the factor pairs of n, weighted by the integer-valued Möbius function—and this recovery relation is equivalent to the original divisor-sum relation.

Möbius inversion
arithmetic functions
divisor sums
Dirichlet convolution
zeta inverse

Exact theorem

Exact Mathlib statement

theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq {R : Type*} [AddCommGroup R] {f g : ℕ → R} : (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd = f n

The theorem at a glance

Möbius Inversion — divisor sums reversed

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

An ivory and forest-green theorem poster displays the positive-index divisor-sum equivalence, a compact divisor lattice, and the checked route through the arithmetic zeta function and its Möbius inverse. — For additive-commutative-group-valued functions on positive naturals, Möbius weighting exactly recovers a function from its divisor sums.

Statement structure

From hypotheses to conclusion

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

A divisor sum produces g(n); ordered factor-pair tiles with ab=n then pair μ(aᵢ) with g(bᵢ) and sum to f(n). — Divisor summation is inverted by Möbius weighting over ordered factor pairs (a,b) with ab=n.

Why it matters

A mathematical landmark

Möbius inversion is a basic change-of-coordinates principle for arithmetic data: cumulative information over divisors can be recovered exactly through the convolution inverse of the constant-one arithmetic function. It underlies multiplicative number theory, inclusion–exclusion on divisibility, and many transformations of arithmetic functions.

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 additive-commutative-group form of Möbius inversion. For functions f, g : ℕ → R and every positive n, it identifies the divisor-sum relation g(n) = ∑_{d ∣ n} f(d) with recovery of f(n) by the Möbius-weighted sum over ordered factor pairs in n.divisorsAntidiagonal. The integer-valued Möbius function acts on R by scalar multiplication. The declaration excludes n = 0 and is not every informal inversion formulation.

The selected statement ranges only over positive natural n; it does not assert either relation at n = 0.
The codomain is an additive commutative group, and the integer-valued Möbius function acts by scalar multiplication.
The recovery sum uses n.divisorsAntidiagonal, whose entries are ordered factor pairs; it is not written as a plain sum over an unspecified index.
This declaration is one precise additive form of Möbius inversion, not a claim for every informal inversion formula.
ProofAtlas is indexing an existing Mathlib theorem, not claiming new mathematics.

Source and local evidence

Where the theorem comes from

Existing declaration: ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq in mathlib
Relationship: The checked artifact is the upstream declaration itself
Local Lean evidence: artifact.library.mathlib.mobius-inversion.v001
Source: Open the pinned upstream reference