feat(number_theory/bernoulli): simplify bernoulli power series

[mo271]

Now using exp_bernoulli_poly to prove both bernoulli'_power_series_mul_exp_sub_one and
bernoulli_power_series_mul_exp_sub_one

---

• depends on: [Merged by Bors] - feat(polynomial/algebra_map): aeval_algebra_map_apply #6649

[mo271]

This change was suggest here: #6309 (comment).
Currently two thing need to be done:

• Avoid circular imports: I moved bernoulli'_power_series_mul_exp_sub_one,
  bernoulli_power_series_mul_exp_sub_one, bernoulli_power_series and bernoulli'_power_series to the file bernoulli_polynomial.lean. This results in problems in the file bernoulli.lean because bernoulli'_odd_eq_zero uses bernoulli'_power_series_mul_exp_sub_one. How to resolve that best?
  I guess one way would be to put bernoulli'_odd_eq_zero and everthing that depends on it to bernoulli_polynomial, but maybe there are better ways,
• There are two lemmas that seem so simple that I would have expected that they exists already, and I simply didn't find them.
  (on going discussion here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/poly.20(a)eval.20and.20algebra.20maps )

[mo271]

help wanted for the question above about where to put this best in order to avoid circular dependencies!

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(polynomial/algebra_map): aeval_algebra_map_apply #6649

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[mo271]

I looked at this again and was surprised that bernoulli_odd_eq_zero uses bernoulli'_power_series_mul_exp_sub_one. Unfortunately, this leads to a circular dependence like this where each line depends on the one before:

• sum_bernoulli
• bernoulli_eq_bernoulli'_of_ne_one
• bernoulli_odd_eq_zero
• bernoulli'_power_series_mul_exp_sub_one
• exp_bernoulli_poly
• sum_bernoulli_poly
• sum_bernoulli
  This means that unless we come up with a way to break this chain somehow, we should stick with the longer proof that we currently have for bernoulli'_power_series_mul_exp_sub_one.