Commit 2021-02-04 21:33 1ee00c89

View on Github →

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.

Estimated changes

Modified src/algebra/big_operators/nat_antidiagonal.lean

added theorem finset.nat.prod_antidiagonal_eq_prod_range_succ_mk

Modified src/data/nat/choose/basic.lean

added theorem nat.add_choose

added theorem nat.factorial_mul_factorial_dvd_factorial_add

Modified src/number_theory/bernoulli.lean

added theorem bernoulli_power_series

added theorem bernoulli_spec'

added theorem bernoulli_spec

Modified src/ring_theory/power_series/well_known.lean

added theorem power_series.constant_coeff_exp