Commit 2021-02-16 12:05 d3c56678

feat(number_theory/bernoulli): the odd Bernoulli numbers (greater than 1) are zero (#6056) The proof requires a ring homomorphism between power series to be defined, eval_mul_hom . This PR defines it and states some of its properties, along with the result that e^(ax) * e^(bx) = e^((a + b) x), which is needed for the final result, bernoulli_odd_eq_zero.