Theorems · Theorem · number theory

ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on

∀ {R : Type u_1} [inst : NonAssocRing R] {f g : ℕ → R} (s : Set ℕ),
  (∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) →
    ((∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔
      ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * g x.2 = f n)

Möbius inversion for functions to a Ring, where the equalities only hold on a well-behaved set.

Defined in

Mathlib.NumberTheory.ArithmeticFunction.Moebius

Cited by

1 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonAssocRing