mathlib3

43041277 - feat(ring_theory/power_series): teach simp to simplify more coercions of polynomials to power series (#11287)

feat(ring_theory/power_series): teach simp to simplify more coercions of polynomials to power series (#11287) So that simp can prove that the polynomial `5 * X^2 + X + 1` coerced to a power series is the same thing with the power series generator `X`. Likewise for `mv_power_series`.