English
Let s be a set with divisibility-closure. For a Nonassociative Ring R and f,g : N → R, the sum identity ∑_{i|n} f(i) = g(n) on s is equivalent to ∑_{x∈n.divisorsAntidiagonal} (μ x.fst : R) * g x.snd = f(n) on s.
Русский
Пусть s замкну по делимости. Для кольца без ассоциативности R и функций f,g: N → R равенство сумм по делителям на множестве 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} (\mu x.fst : R) * g x.snd) = f(n)).$$
Lean4
/-- Möbius inversion for functions to a `Ring`, where the equalities only hold on a well-behaved
set. -/
theorem sum_eq_iff_sum_mul_moebius_eq_on [NonAssocRing 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, (μ x.fst : R) * g x.snd) = f n :=
by
rw [sum_eq_iff_sum_smul_moebius_eq_on s hs]
apply forall_congr'
intro a; refine imp_congr_right ?_
refine fun _ => imp_congr_right fun _ => (sum_congr rfl fun x _hx => ?_).congr_left
rw [zsmul_eq_mul]
