mathlib3
4a3b22e5 - feat(number_theory/bernoulli_polynomials): Derivative of Bernoulli polynomial (#14625)

Commit
3 years ago
feat(number_theory/bernoulli_polynomials): Derivative of Bernoulli polynomial (#14625) Add the statement that the derivative of `bernoulli k x` is `k * bernoulli (k-1) x`. This will be used in a subsequent PR to evaluate the even positive integer values of the Riemann zeta function.
Author
Parents
Loading