English
Let s be a set of naturals closed under divisibility. For a commutative group with zero, the equality of divisor products with regular multiplication is equivalent to the corresponding antidiagonal product with Möbius exponents, under nonzero hypotheses.
Русский
Пусть s замкну по делимости. Для коммутативной группы с нулём эквивалентны равенства: произведение по делителям равно, и равенство антидиагонального произведения с μ-возведениями к степеням, при ненулевых условиях.
LaTeX
$$$\forall f,g : \mathbb{N} \to R\ (s:Set\mathbb{N}) (hs : ∀ m n, m \mid n → n ∈ s → m ∈ s) : (∀ n > 0, n ∈ s → (\sum i ∈ n.divisors, f(i)) = g(n)) \\iff \\ (∀ n > 0, n ∈ s → (\sum x ∈ n.divisorsAntidiagonal, (μ x.fst : R) * g x.snd) = f(n)).$$
Lean4
/-- Möbius inversion for functions to a `CommGroupWithZero`, where the equalities only hold on
a well-behaved set. -/
theorem prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero [CommGroupWithZero R] (s : Set ℕ)
(hs : ∀ m n, m ∣ n → n ∈ s → m ∈ s) {f g : ℕ → R} (hf : ∀ n > 0, f n ≠ 0) (hg : ∀ n > 0, g n ≠ 0) :
(∀ 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 :=
by
refine
Iff.trans
(Iff.trans (forall_congr' fun n => ?_)
(@prod_eq_iff_prod_pow_moebius_eq_on 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) s hs))
(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]
