English
Let s be a set and hs describe divisibility-closure. Then for AddCommGroup-valued f,g the statement ∑_{i∈divisors(n)} f(i) = g(n) for all n in s is equivalent to ∑_{x∈divisorsAntidiagonal(n)} μ(x.fst) • g(x.snd) = f(n) for all n in s.
Русский
Пусть s — множество и hs задаёт замкнутость по делимости. Тогда для значений в AddCommGroup: ∑_{i|n} f(i) = g(n) при всех n∈s эквивалентно ∑_{x∈n.antidiagonal} μ(x.fst) • g(x.snd) = f(n) для всех n∈s.
LaTeX
$$$\forall f,g : \mathbb{N} \to R\, (s:Set\mathbb{N})\ (hs : ∀ m n, m \mid n → n ∈ s → m ∈ s) : (∀ n ∈ s, (\sum i ∈ n.divisors, f i) = g n) \iff \forall n ∈ s, (\sum x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd) = f n$$$
Lean4
/-- The Bernoulli numbers:
the $n$-th Bernoulli number $B_n$ is defined recursively via
$$B_n = 1 - \sum_{k < n} \binom{n}{k}\frac{B_k}{n+1-k}$$ -/
def bernoulli' (n : ℕ) : ℚ :=
1 - ∑ k : Fin n, n.choose k / (n - k + 1) * bernoulli' k
