feat(ring_theory/power_series/basic): coeff_succ_X_mul (#6370)
feat(ring_theory/power_series/basic): coeff_succ_X_mul (#6370)




Co-authored-by: Moritz Firsching <c8f1a6aabac1f1b3e5245c40ceca966f954711d2@google.com>

leanprover-community/mathlib,leanprover-community/mathlib