English
For a NonAssociative Ring R, a set s closed under divisibility, and f,g: N → R, the equivalence holds between the divisor-sum identity and the antidiagonal μ-weighted sum identity using ordinary multiplication.
Русский
Для кольца без ассоциативности R и множества s, замкнутого по делимости, верна эквивалентность между равенством по делителям и суммой по антидиагонали с весами μ(d) умножения.
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
theorem bernoulli'_def (n : ℕ) : bernoulli' n = 1 - ∑ k ∈ range n, n.choose k / (n - k + 1) * bernoulli' k := by
rw [bernoulli'_def', ← Fin.sum_univ_eq_sum_range]
