Theorems · Theorem · number theory

ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on

∀ {R : Type u_1} [inst : AddCommGroup 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 an AddCommGroup, where the equalities only hold on a well-behaved set.

Defined in

Mathlib.NumberTheory.ArithmeticFunction.Moebius

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommGroup