Bernoulli numbers
The Bernoulli numbers are a sequence of numbers that frequently show up in number theory.
For example, they show up in the Taylor series of many trigonometric and hyperbolic functions,
and also as (integral multiples of products of powers of π and)
special values of the Riemann zeta function.
(Note: these facts are not yet available in mathlib)
In this file, we provide the definition,
and the basic fact (sum_bernoulli) that
$$ \sum_{k < n} \binom{n}{k} * B_k = n, $$
where $B_k$ denotes the the $k$-th Bernoulli number.
The Bernoulli numbers: the $n$-th Bernoulli number $B_n$ is defined recursively via $$B_n = \sum_{k < n} \binom{n}{k} * \frac{B_k}{n+1-k}$$