mathlib3

feat(ring_theory/power_series): several simp lemmas

#1945

Merged