feat(Analysis): binomial series convergence

[vasnesterov]

This PR introduces the binomial series (as FormalMultilinearSeries) for an algebra over a field of characteristic zero.

Main Results:

• binomialSeries_radius_ge_one: The radius of convergence of the binomial series is at least 1.
• one_add_rpow_hasFPowerSeriesAt_zero: For real a and |x| < 1, the binomial series ∑ k, (Ring.choose a k) * x^k converges to (1 + x).rpow a. Here I use this proof in which one shows that the series and the (1 + x)^a function satisfy the same ODE.

---

• depends on: [Merged by Bors] - feat(Analysis/Analytic): lemmas about smul for power series #19816
• depends on: [Merged by Bors] - feat(Analysis/Analytic): FormalMultilinearSeries.unshift convergence #19848

I added the Mathlib.Tactic.MoveAdd import to noshake, as it attempts to remove this import even though it is required for the move_mul tactic.

This PR is necessary for my tactic (#18486), which computes the asymptotics of real functions, where I use the binomial series to approximate real powers of functions.