Theorems · Theorem · number theory

ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq

∀ {R : Type u_1} [inst : AddCommGroup R] {f g : ℕ → R},
  (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 • g x.2 = f n

Möbius inversion for functions to an AddCommGroup.

Defined in: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Cited by: 3 results in Mathlib
Foundations: Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
AddCommGroupstatement and proof · cited by 12,871
Finset.sumstatement and proof · cited by 5,195
Finset.sum_congrproof · cited by 2,323
LT.lt.ne'proof · cited by 1,417
one_smulproof · cited by 1,374
ArithmeticFunctionstatement and proof · cited by 290
Nat.divisorsstatement and proof · cited by 137
Nat.divisorsAntidiagonalstatement and proof · cited by 61
ArithmeticFunction.zetaproof · cited by 45
ArithmeticFunction.moebiusstatement and proof · cited by 45
ArithmeticFunction.map_zeroproof · cited by 34

Cited by3

Results whose statement or proof uses this declaration.

ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_onproof · cited by 3
ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eqproof · cited by 1
ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eqproof · cited by 0