English
For a commutative group G, and subsets s of natural numbers closed under divisibility, the divisor product equality holds with powers of g according to μ on the antidiagonal: ∀ n>0, n∈s → ∏_{i|n} f(i) = g(n) iff ∀ n>0, n∈s → ∏_{(d,e): de=n} g(e)^{μ(d)} = f(n).
Русский
Для коммутативной группы G и множества s ⊆ N, замкнутого по делимости, равенство произведений по делителям эквивалентно: ∀ n>0, n∈s, ∏_{i|n} f(i) = g(n) тогда и только тогда, ∏_{(d,e): de=n} g(e)^{μ(d)} = f(n).
LaTeX
$$$\forall f,g : \mathbb{N} \to G\, (s:Set\mathbb{N}) (hs : ∀ m n, m \mid n → n ∈ s → m ∈ s) : (∀ n > 0, n ∈ s → (\prod_{i ∈ n.divisors} f(i)) = g(n)) \\iff \\ (∀ n > 0, n ∈ s → (\prod_{x ∈ n.divisorsAntidiagonal} g(x.snd)^{ μ x.fst}) = f(n)).$$
Lean4
/-- Möbius inversion for functions to a `CommGroup`, where the equalities only hold on a
well-behaved set. -/
theorem prod_eq_iff_prod_pow_moebius_eq_on [CommGroup R] {f g : ℕ → R} (s : Set ℕ) (hs : ∀ 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, g x.snd ^ μ x.fst) = f n :=
@sum_eq_iff_sum_smul_moebius_eq_on (Additive R) _ _ _ s hs
