English
Let s ⊆ N with 0 ∉ s and hs the divisibility-closure. Then ∀ n ∈ s, (∑_{i|n} f(i)) = g(n) iff ∀ n ∈ s, (∑_{x ∈ n.divisorsAntidiagonal} μ(x.fst) • g(x.snd)) = f(n).
Русский
Пусть s ⊆ N, 0 ∉ s и hs выполняется. Тогда для n∈s выполняется равенство ∑_{i|n} f(i) = g(n) эквивалентно ∑_{x∈n.divisorsAntidiagonal} μ(x.fst) • g(x.snd) = f(n).
LaTeX
$$$\forall f,g : \mathbb{N} \to R\, (s:Set\mathbb{N}) (hs : ∀ m n, m \mid n → n ∈ s → m ∈ s) (hs0 : 0 ∉ s) : (∀ n ∈ s, (\sum i ∈ n.divisors, f i) = g n) \iff ∀ n ∈ s, (\sum x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd) = f n$$$
Lean4
theorem bernoulli'_def' (n : ℕ) : bernoulli' n = 1 - ∑ k : Fin n, n.choose k / (n - k + 1) * bernoulli' k := by
rw [bernoulli']
