Theorems · Theorem · number theory

ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq

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

Möbius inversion for functions to a CommGroup.

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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

DFunLike.coestatement · cited by 62,936
Finset.prodstatement · cited by 2,356
CommGroupstatement and proof · cited by 990
ArithmeticFunctionstatement · cited by 290
Nat.divisorsstatement · cited by 137
Nat.divisorsAntidiagonalstatement · cited by 61
ArithmeticFunction.moebiusstatement · cited by 45
ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eqproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzeroproof · cited by 1