mathlib3

1ee00c89 - feat(number_theory/bernoulli): Results regarding Bernoulli numbers as a generating function (#5957)

feat(number_theory/bernoulli): Results regarding Bernoulli numbers as a generating function (#5957) We prove that the Bernoulli numbers are generating functions for t/(e^t - 1). Most of the results are proved by @kbuzzard. Co-authored-by: laughinggas <58670661+laughinggas@users.noreply.github.com>