English
Let f, g be functions from the natural numbers to a commutative group with zero, and assume f(n) ≠ 0 and g(n) ≠ 0 for every n > 0. Then for all n > 0, the product of f over all divisors of n equals g(n) if and only if the product over all divisor pairs (d, e) with d⋅e = n of g(e) raised to the Möbius function μ(d) equals f(n).
Русский
Пусть f, g — функции from натуральных чисел в коммутативную группу с нулём, при этом f(n) ≠ 0 и g(n) ≠ 0 для каждого n > 0. Тогда для каждого n > 0 выполняется эквивалентность: произведение f(i) по всем делителям i числа n равно g(n) тогда и только тогда, когда произведение по всем парам делителей (d, e) с de = n отдается равной g(e) под возведением в степень μ(d), равно f(n).
LaTeX
$$$\forall f,g : \mathbb{N} \to R\,(hf:\forall n>0, f(n) \neq 0)\,(hg:\forall n>0, g(n) \neq 0)\,\forall n>0,\ (\prod_{i\mid n} f(i) = g(n)) \ \Longleftrightarrow \ \forall n>0,\ \prod_{(d,e): de=n} g(e)^{\mu(d)} = f(n)$.$$
Lean4
/-- Möbius inversion for functions to a `CommGroupWithZero`. -/
theorem prod_eq_iff_prod_pow_moebius_eq_of_nonzero [CommGroupWithZero R] {f g : ℕ → R} (hf : ∀ n : ℕ, 0 < n → f n ≠ 0)
(hg : ∀ n : ℕ, 0 < n → g n ≠ 0) :
(∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.snd ^ μ x.fst = f n :=
by
refine
Iff.trans
(Iff.trans (forall_congr' fun n => ?_)
(@prod_eq_iff_prod_pow_moebius_eq Rˣ _ (fun n => if h : 0 < n then Units.mk0 (f n) (hf n h) else 1) fun n =>
if h : 0 < n then Units.mk0 (g n) (hg n h) else 1))
(forall_congr' fun n => ?_) <;>
refine imp_congr_right fun hn => ?_
· dsimp
rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0, prod_congr rfl _]
intro x hx
rw [dif_pos (Nat.pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]
· dsimp
rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0, prod_congr rfl _]
intro x hx
rw [dif_pos (Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal hx)), Units.coeHom_apply,
Units.val_zpow_eq_zpow_val, Units.val_mk0]
