Public Mathlib landmark · existing upstream theorem · read-only
ProofAtlas

Number theory · existing Mathlib declaration

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.

The theorem at a glance

Möbius Inversion — divisor sums reversed

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

For additive-commutative-group-valued functions on positive naturals, Möbius weighting exactly recovers a function from its divisor sums. Generated explanation only; the exact HTML statement and pinned source are authoritative.
Detailed visual description

The poster presents the selected equivalence without flattening its ordered-factor-pair recovery sum. A sparse central engraving moves from divisor aggregation to signed cancellation, while a short route names the zeta action, Möbius action, and two-sided inverse identity used in the Mathlib proof.

Formal orientation

Statement map

Statement map for Möbius InversionDivisor summation by the arithmetic zeta function is inverted by Möbius weighting on ordered factor pairs. The pinned upstream declaration is ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq. The exact checked statement is 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.Mathematical readingDivisor summation by thearithmetic zeta functionis inverted by Möbiusweighting on orderedfactor pairs.Pinned declarationmathlib ·ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eqExact checked formtheoremArithmeticFunction.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 nStatement map for Möbius InversionDivisor summation by the arithmetic zeta function is inverted by Möbius weighting on ordered factor pairs. The pinned upstream declaration is ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq. The exact checked statement is 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.Mathematical readingDivisor summation by thearithmetic zeta functionis inverted by Möbiusweighting on orderedfactor pairs.Pinned declarationmathlib ·ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eqExact checked formtheoremArithmeticFunction.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

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

Divisor summation is inverted by Möbius weighting over ordered factor pairs (a,b) with ab=n. Scientific diagram · explanatory, not proof evidence.
Detailed visual description

The upper stage shows g(n) as a divisor sum of f(d). The recovery stage uses distinct variables on every ordered factor-pair tile and states the exact compact relation ∑_{ab=n} μ(a)·g(b)=f(n).

Complementary intuition

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.

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 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
Selected evidence declaration text
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

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 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.

Provenance

Origin and evidence stay separate

Existing declaration
ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq in mathlib
Relationship
The checked artifact is the upstream declaration itself
Preferred checked artifact
artifact.library.mathlib.mobius-inversion.v001
Source handling
Verified upstream reference; no mirrored source package